Internal Universes in Models of Homotopy Type Theory

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.

In H. Kirchner (ed), Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Leibniz International Proceedings in Informatics (LIPIcs), Vol. 108, pp. 22:1-22:17, 2018

References in corpus (4)

• The Equivalence Extension Property and Model Structures
• A type theory for synthetic $\infty$-categories
• Cubical sets and the topological topos
• Decomposing the Univalence Axiom

Cited by in corpus (11)

• A General Framework for the Semantics of Type Theory
• Staged Compilation with Two-Level Type Theory
• Axioms for Modelling Cubical Type Theory in a Topos
• Dual-Context Calculi for Modal Logic
• Semantics of multimodal adjoint type theory
• Substructural fixed-point theorems and the diagonal argument: theme and variations
• A Categorical Normalization Proof for the Modal Lambda-Calculus
• Constructing Initial Algebras Using Inflationary Iteration
• Canonicity and homotopy canonicity for cubical type theory
• Unifying cubical and multimodal type theory
• Relative elegance and cartesian cubes with one connection