* Internal Universes in Models of Homotopy Type Theory
@ 2018-01-24 13:10 Bas Spitters
0 siblings, 0 replies; only message in thread
From: Bas Spitters @ 2018-01-24 13:10 UTC (permalink / raw)
To: homotopytypetheory
Our paper has just appeared on the arxiv:
Internal Universes in Models of Homotopy Type Theory
http://arxiv.org/abs/1801.07664
Dan, Ian, Andy, Bas
---
Internal Universes in Models of Homotopy Type Theory
Authors: Daniel R. Licata, Ian Orton, Andrew M. Pitts and 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.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2018-01-24 13:10 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-01-24 13:10 Internal Universes in Models of Homotopy Type Theory Bas Spitters
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).