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

Abstract

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.