External univalence for second-order generalized algebraic theories
share
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 à la Tarski, the univalence axiom, the Uniqueness of Identity Proofs axiom, etc.
READ FULL TEXT