Rzk: A Proof Assistant for Synthetic ∞-Categories
5 hours ago
- #Directed Type Theory
- #Proof Assistant
- #Synthetic ∞-Categories
- Rzk 是一个证明助手，它实现了 Riehl 和 Shulman 的单纯型理论 (RSTT) 的一个改进版本，用于 ∞-范畴的合成推理。
- 它提供了 RSTT 的一个计算变体，旨在进行实用的类型检查，并包含诸如形状逻辑自动证明器等特性。
- 从 RSTT 到 Rzk 的翻译是合理的，具有忠实性（每个 RSTT 证明都可翻译）和保守性（Rzk 不会证明关于 RSTT 类型的任何新内容）。
- 该论文包含一个在 Rzk 中进行证明的教程式介绍，并描述了其实现，涵盖了类型检查算法和自动化工具。