  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.
