Modal Descent

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 $◯$-'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 $◯$-'etale maps to prove a modal descent theorem: a map with modal fibers into $◯X$ is the same thing as a $◯$-'etale map into a type $X$. We conclude with an application to real-cohesive homotopy type theory and remarks how $◯$-'etale maps relate to the formally etale maps from algebraic geometry.