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

TL;DR

This paper develops a 2-categorical semantics for axiomatic dependent type theory with computation axioms, extending Garner's approach and showing the non-admissibility of certain computation rules.

Contribution

It introduces a 2-categorical model for axiomatic type theory, relaxing Garner's conditions and providing a semantic proof regarding computation rules.

Findings

Semantic interpretation of axiomatic theories is well-defined and sound.

Axiomatic identity types do not admit certain computation rules.

Extension of Garner's 2-categorical approach to axiomatic settings.

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.