## Authors: Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters

## Paper Information

Title: | Internal Universes in Models of Homotopy Type Theory |

Authors: | Daniel R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters |

Proceedings: | FSCD Presented Papers |

Editor: | Helene Kirchner |

Keywords: | cubical sets, dependent type theory, homotopy type theory, internal language, modalities, univalent foundations, universes |

Abstract: | ABSTRACT. 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Ă¶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 a completely internal development of models of homotopy type theory within what we call crisp type theory. |

Pages: | 17 |

Talk: | Jul 10 10:00 (Session 52B: Types) |

Paper: |