Internal Universes in Models of Homotopy Type Theory

TL;DR

This paper introduces a modal extension to the internal language of models of homotopy type theory, enabling the construction and axiomatization of universes that classify fibrations, exemplified by the cubical sets model.

Contribution

It presents a novel modal extension called crisp type theory that allows internal axiomatization of universes in homotopy type theory models, including the cubical sets model.

Findings

Constructed a universe classifying CCHM fibrations using tiny interval assumption.

Extended internal language with a modal operator for global element properties.

Provided an elementary axiomatization of models within crisp type theory.

Abstract

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-M\"ortberg (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.