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 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.

On some orthogonal factorization systems

The orthogonality relation between arrows in the class of all morphisms of a given category C yields a "concrete" antitone Galois connection between the class of all subclasses of morphisms of C. For a class Σ of morphisms of C, we denote by ⊥Σ (resp., Σ⊥) the class of all morphisms f in C such that f ⊥ g (resp., g ⊥ f) for each morphism g in Σ. A couple (Σ, Γ) of classes of morphisms is said to be an (orthogonal) prefactorization system if If, in addition the pfs satisfies then it will be called a dense prefactorization system. A pair [Formula: see text] of classes of morphisms in a category C is called an (orthogonal) factorization system if it is a prefactorization system and each morphism f in C has a factorization f = me, with [Formula: see text] and [Formula: see text]. This paper provides several examples of factorization systems and dense factorization systems in the category Top of topological spaces.