AI 中文总结
介绍用于合成∞-范畴的证明助手Rzk，它实现了RSTT的细化。定义从RSTT到Rzk的合理翻译，包括忠实性和保守性证明。还给出在Rzk中证明的教程及实现描述，含类型检查算法和自动证明器。
AI 中文摘要
同伦类型论（HoTT）是一种允许对∞-群胚进行合成推理的类型论。一些证明助手（如Rocq和Agda）实现了HoTT的变体。有向类型论是用于对∞-范畴进行合成推理的类型论，其中一维态射（或路径）不一定可逆。在有向类型论的提议中，最成熟的是基于有向区间和三角形等单纯形形状的Riehl和Shulman的单纯形类型论（RSTT）。我们展示了Rzk，一个实现（RSTT的细化）用于对∞-范畴进行合成推理的证明助手。具体而言，Rzk实现的类型论是RSTT的计算变体，经调整以实现实用的类型检查。我们定义了从RSTT到Rzk的翻译，并证明它是合理的：每个RSTT证明都能翻译成Rzk证明（忠实性），且Rzk不会证明关于RSTT类型的新内容（保守性）。我们还给出了在Rzk中证明的教程介绍，并描述了其实现，包括类型检查算法和形状逻辑的自动证明器。
英文摘要
Homotopy type theory (HoTT) is a type theory that allows for synthetic reasoning about $\infty$-groupoids. Several proof assistants (such as Rocq and Agda) implement variants of HoTT. Directed type theory is a type theory for synthetic reasoning about $\infty$-categories, where morphisms (or paths) of dimension 1 are not necessarily invertible. Among the proposals for directed type theory, the most developed is Riehl and Shulman's simplicial type theory (RSTT), based on simplicial shapes such as directed intervals and triangles. We present Rzk, a proof assistant implementing (a refinement of) RSTT for synthetic reasoning about $\infty$-categories. Specifically, the type theory implemented by Rzk is a computational variant of RSTT adjusted to make type checking practical. We define a translation from RSTT to Rzk and prove that it is sensible: every RSTT proof translates to an Rzk proof (faithfulness), and Rzk proves nothing new about RSTT types (conservativity). We also give a tutorial introduction to proving in Rzk, and describe its implementation, including the type-checking algorithm and the automated prover for the logic of shapes.
Comments54 pages, including appendices. Describes Rzk v0.7.8. Ancillary files include the code of every example in the paper and the scripts and trace behind the evaluation
