Axioms for Modelling Cubical Type Theory in a Topos
The homotopical approach to intensional type theory views proofs of
equality as paths. We explore what is required of an interval-like
object I in a topos to give a model of type theory in which
elements of identity types are functions with domain I.
Cohen, Coquand, Huber and Mörtberg give such a model using a
particular category of presheaves. We investigate the extent to which
their model construction can be expressed in the internal type theory
of any topos and identify a collection of quite weak axioms for this
purpose. This clarifies the definition and properties of the notion of
uniform Kan filling that lies at the heart of their constructive
interpretation of Voevodsky's univalence axiom. Furthermore, since our
axioms can be satisfied in a number of different ways, we show that
there is a range of topos-theoretic models of homotopy type theory in
this style.