Internal Universes in Models of Homotopy Type Theory

Research output: Other contributionNet publication - Internet publicationResearch



We show that universes of fibrations in various models of homotopy type theory have an essentially global character: they cannot be described in the internal language of the presheaf topos from which the model is 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 a completely internal development of models of homotopy type theory within what we call crisp type theory.
Original languageEnglish
Publication year23 Jan 2018
Number of pages17
StatePublished - 23 Jan 2018

    Research areas

  • cs.LO, F.4.1; F.3.2

See relations at Aarhus University Citationformats

Download statistics

No data available

ID: 121317800