标题： 2-范畴论方法在具有计算公理的依赖类型理论语义中的应用 显示英文标题

标题： A 2-categorical approach to the semantics of dependent type theory with computation axioms

摘要： 公理类型理论是一种没有计算规则的依赖类型理论。 通常表征这些规则的项等式判断被替换为计算公理，即由同伦类型定义的额外项判断。 本文致力于从高范畴论的角度提供其语义的有效描述：鉴于将可意类型形成器编码为一维范畴术语和性质的挑战，即使对于公理类型形成器来说这一挑战依然存在，我们采用理查德·加纳在依赖类型二维研究中的方法。 我们证明，公理理论的类型形成器可以编码为自然的二维范畴理论数据，通过称为显示映射二维范畴的二维范畴模型来呈现公理类型理论的语义。 在公理情况下，加纳为解释可意类型形成器所确定的二维范畴要求被放宽。 因此，我们获得了一个公理理论语义的表述，该表述推广了加纳对可意情况的表述。 我们的主要结果指出，在显示映射二维范畴中对公理理论的解释是定义良好的，并且具有合理性属性。 我们利用这一事实提供了一个语义证明，说明可意同伦类型的计算规则在公理类型理论中是不可接受的。 这是通过重新审视霍夫曼和斯特赖彻的群胚模型实现的，该模型认为公理同伦类型但不认为可意同伦类型。 显示英文摘要

摘要： Axiomatic type theory is a dependent type theory without computation rules. The term equality judgements that usually characterise these rules are replaced by computation axioms, i.e., additional term judgements that are typed by identity types. This paper is devoted to providing an effective description of its semantics, from a higher categorical perspective: given the challenge of encoding intensional type formers into 1-dimensional categorical terms and properties, a challenge that persists even for axiomatic type formers, we adopt Richard Garner's approach in the 2-dimensional study of dependent types. We prove that the type formers of axiomatic theories can be encoded into natural 2-dimensional category theoretic data, obtaining a presentation of the semantics of axiomatic type theory via 2-categorical models called display map 2-categories. In the axiomatic case, the 2-categorical requirements identified by Garner for interpreting intensional type formers are relaxed. Therefore, we obtain a presentation of the semantics of the axiomatic theory that generalises Garner's one for the intensional case. Our main result states that the interpretation of axiomatic theories within display map 2-categories is well-defined and enjoys the soundness property. We use this fact to provide a semantic proof that the computation rule of intensional identity types is not admissible in axiomatic type theory. This is achieved via a revisitation of Hofmann and Streicher's groupoid model that believes axiomatic identity types but does not believe intensional ones.