Rzk: A Proof Assistant for Synthetic ∞-Categories
5 hours ago
- #Directed Type Theory
- #Proof Assistant
- #Synthetic ∞-Categories
- Rzk is a proof assistant implementing a refinement of Riehl and Shulman's simplicial type theory (RSTT) for synthetic reasoning about ∞-categories.
- It provides a computational variant of RSTT designed for practical type checking and includes features like an automated prover for shape logic.
- The translation from RSTT to Rzk is sensible, being faithful (every RSTT proof translates) and conservative (Rzk proves nothing new about RSTT types).
- The paper includes a tutorial introduction to proving in Rzk and describes its implementation, covering type-checking algorithms and automated tools.