Modalities in homotopy type theory

Abstract

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

References in corpus (7)

• The Simplicial Model of Univalent Foundations (after Voevodsky)
• The local universes model: an overlooked coherence construction for dependent type theories
• Sets in homotopy type theory
• The join construction
• Univalence in locally cartesian closed infinity-categories
• Higher Homotopies in a Hierarchy of Univalent Universes
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

Cited by in corpus (16)

• The join construction
• Notes on Clans and Tribes
• Left-exact Localizations of $\infty$-Topoi I: Higher Sheaves
• Modal Descent
• Higher prequantum geometry
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• Indexed type theories
• Modal Fracture of Higher Groups
• Non-accessible localizations
• Fitch-Style Modal Lambda Calculi
• $L^{\prime }$-localization in an $\infty$-topos
• Partial Functions and Recursion in Univalent Type Theory
• Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT
• Epimorphisms and Acyclic Types in Univalent Foundations
• Smooth and Proper Maps
• Curry-Howard-Lambek Correspondence for Intuitionistic Belief