Internal Universes in Models of Homotopy Type Theory

Daniel R. Licata, Ian Orton, Andrew M. Pitts, Bas Spitters

Publikation: AndetUdgivelser på nettet - Net-publikationForskningpeer review

36 Citationer (Scopus)
149 Downloads (Pure)

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ö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.

OriginalsprogEngelsk
Publikationsdato1 jul. 2018
Udgiverarxiv.org
Antal sider17
ISBN (Elektronisk)9783959770774
StatusUdgivet - 1 jul. 2018
NavnarXiv

Fingeraftryk

Dyk ned i forskningsemnerne om 'Internal Universes in Models of Homotopy Type Theory'. Sammen danner de et unikt fingeraftryk.

Citationsformater