Synthetic 1-Categories in Directed Type Theory
Thorsten Altenkirch and Jacob Neumann
定向类型理论领域寻求设计能够合成(更高)类别推理的类型理论,通过将Martin-Löf类型理论的对称身份类型进行概括为不对称的hom-types。 我们阐明了类别模型的定向类型理论,具有跟踪方差的适当模式和一个强大的定向J规则,能够证明关于hom类型的任意术语的结果;我们把这条规则用于在合成1类理论中制作几种结构。 因为这个理论完全用广义的代数理论来表达,我们自动知道这种定向类型理论承认语法模型,是指向更高观测类型理论的第一步。
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synt...