Decomposing the Univalence Axiom
This paper investigates Voevodsky's univalence axiom in intensional
Martin-Löf type theory. In particular, it looks at how univalence
can be derived from simpler axioms. We first present some existing
work, collected together from various published and unpublished
sources; we then present a new decomposition of the univalence axiom
into simpler axioms. We argue that these axioms are easier to verify
in certain potential models of univalent type theory, particularly
those models based on cubical sets. Finally we show how this
decomposition is relevant to an open problem in type theory.