Internal Universes in Models of Homotopy Type Theory
We begin by recalling the essentially global character of universes in
various models of homotopy type theory, which prevents a
straightforward axiomatization of their properties using the
internal language of the presheaf toposes from which these model are
constructed. We get around this problem by extending the internal
language with a modal operator for expressing properties of global
elements. In this setting we show how to construct a universe that
classifies the Cohen-Coquand-Huber-MoĢrtberg (CCHM) notion of
fibration from their cubical sets model, starting from the
assumption that the interval is tiny - a property that the interval
in cubical sets does indeed have. This leads to an elementary
axiomatization of that and related models of homotopy type theory
within what we call crisp type theory.