# 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*.