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 $\bigcirc$-equivalences and the right class is the class of $\bigcirc$-\'etale 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$-\'etale maps are the maps that are right orthogonal to the map $\mathbf{1} \to \mathbf{S}^{n+1}$. We use the $\bigcirc$-\'etale maps to prove a modal descent theorem: a map with modal fibers into $\bigcirc X$ is the same thing as a $\bigcirc$-\'etale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remarks how $\bigcirc$-\'etale maps relate to the formally etale maps from algebraic geometry.