External univalence for second-order generalized algebraic theories

TL;DR

This paper introduces external univalence, a property capturing the preservation of equivalences in second-order generalized algebraic theories, providing a syntactic and semantic framework applicable to various type theories.

Contribution

It defines external univalence for theories, offers syntactic criteria to verify it, and proves it for several important theories including dependent type theory with standard axioms.

Findings

External univalence captures preservation of equivalences in theories.

Syntactic conditions can verify external univalence.

Proven for theories like categories and dependent type theory.

Abstract

Voevodsky's univalence axiom is often motivated as a realization of the equivalence principle; the idea that equivalent mathematical structures satisfy the same properties. Indeed, in Homotopy Type Theory, properties and structures can be transported over type equivalences. However, we may wish to explain the equivalence principle without relying on the univalence axiom. For example, all type formers preserve equivalences in most type theories; thus it should be possible to transport structures over type equivalences even in non-univalent type theories. We define external univalence, a property of type theories (and more general second-order generalized algebraic theories) that captures the preservation of equivalences (or other homotopy relations). This property is defined syntactically, as the existence of identity types on the (syntactically defined) coclassifying (Sigma,Pi_rep)-CwF (also called generic model or walking model) of the theory. Semantically, it corresponds to the existence of some left semi-model structure on the category of models of the theory. We give syntactic conditions that can be used to check that a theory satisfies external univalence. We prove external univalence for some theories, such as the first-order generalized algebraic theory of categories, and dependent type theory with any standard choice of type formers and axioms, including identity types, Sigma-types, Pi-types, universes \`a la Tarski, the univalence axiom, the Uniqueness of Identity Proofs axiom, etc.