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 (2)

• The join construction
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

Cited by in corpus (15)

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