Modal Descent

Abstract

Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated to any modality, of which the left class is the class of $◯$-equivalences and the right class is the class of $◯$-étale maps. This factorization system is called the reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the reflective factorization system of a modality. In the special case of the $n$-truncation the reflective factorization system has a simple description: we show that the $n$-étale maps are the maps that are right orthogonal to the map $1\to {\mathbf{S}}^{n+1}$. We use the $◯$-étale maps to prove a modal descent theorem: a map with modal fibers into $◯X$ is the same thing as a $◯$-étale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remarks how $◯$-étale maps relate to the formally etale maps from algebraic geometry.

References in corpus (5)

• Differential cohomology in a cohesive infinity-topos
• Modalities in homotopy type theory
• Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
• Synthetic geometry of differential equations: I. Jets and comonad structure
• Classifying Types

Cited by in corpus (6)

• Topological Quantum Gates in Homotopy Type Theory
• Small object arguments, plus-construction, and left-exact localizations
• The Quantum Monadology
• Modal Fracture of Higher Groups
• From dependent type theory to higher algebraic structures
• Synthetic G-jet-structures in modal homotopy type theory