Coherence of strict equalities in dependent type theories

Abstract

We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of type theory, we reconstruct Hofmann's proof of the conservativity of Extensional Type Theory over Intensional Type Theory. We generalize these methods to type theories without the Uniqueness of Identity Proofs principle, such as variants of Homotopy Type Theory, by introducing a notion of higher congruence over models of type theory. Our definition of higher congruence is inspired by Brunerie's type-theoretic definition of weak $\infty$-groupoid. For a large class of type theories, we reduce the problem of the conservativity of equational extensions to more tractable acyclicity conditions.

arXiv comment51 pages

References in corpus (10)

• The identity type weak factorisation system
• Two-dimensional models of type theory
• Two-Level Type Theory and Applications
• On the homotopy groups of spheres in homotopy type theory
• On the strength of dependent products in the type theory of Martin-Löf
• The homotopy theory of type theories
• Models of Type Theory with Strict Equality
• Algebraic models of homotopy types and the homotopy hypothesis
• Morita equivalences between algebraic dependent type theories
• Constructive Set Theory from a Weak Tarski Universe

Cited by in corpus (1)

• Quadratic type checking for objective type theory