Internal Universes in Models of Homotopy Type Theory

Research output: ResearchNet publication - Internet publication



  • Daniel R. Licata
    Daniel R. Licata
  • Ian Orton
    Ian Orton
  • Andrew M. Pitts
    Andrew M. Pitts
  • Bas Spitters
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

ID: 121317800