
AbstractAny 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 with 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 modal reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the modal reflective factorization system of a modality. In the special case of the n-truncation, the modal reflective factorization system has a simple description: we show that the n-étale maps are the maps that are right orthogonal to the map $${\rm{1}} \to {\rm{ }}{{\rm{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 remark how ○-étale maps relate to the formally etale maps from algebraic geometry.
FOS: Mathematics, Mathematics - Category Theory, Category Theory (math.CT), 18A32, 03B15, 18F20
FOS: Mathematics, Mathematics - Category Theory, Category Theory (math.CT), 18A32, 03B15, 18F20
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
