(∞,1)-category of (∞,1)-sheaves
Extra stuff, structure and property
locally n-connected (n,1)-topos
locally ∞-connected (∞,1)-topos, ∞-connected (∞,1)-topos
structures in a cohesive (∞,1)-topos
The -connected/-truncated factorization system is an orthogonal factorization system in an (∞,1)-category, specifically in an (∞,1)-topos, that generalizes the relative Postnikov systems of ∞Grpd: it factors any morphism through its (n+2)-image by an (n+2)-epimorphism followed by an (n+2)-monomorphism.
As ranges through these factorization systems form an ∞-ary factorization system.
This appears as a remark in HTT, Example 22.214.171.124. A construction of the factorization in terms of a model category presentation is in (Rezk, prop. 8.5).
For all , the -connected/-truncated factorization system is stable: the class of n-connected morphisms is preserved under (∞,1)-pullback.
This appears as (Lurie, prop. 126.96.36.199(6)).
A (-2)-truncated morphism is precisely an equivalence in an (∞,1)-category (see there or HTT, example 188.8.131.52).
Moreover, every morphism is (-2)-connected.
Therefore for the -connected/-truncated factorization system says (only) that equivalences have inverses, unique up to coherent homotopy.
A (-1)-truncated morphism is precisely a full and faithful morphism.
A (-1)-connected morphism is one whose homotopy fibers are inhabited.
In ∞Grpd a morphism between 0-truncated objects (sets)
Therefore between 0-truncated objects the (-1)-connected/(-1)-truncated factorization system is the epi/mono factorization system and hence image factorization.
Generally, the (-1)-connected/(-1)-truncated factorization is through the -categorical 1-image, the homotopy image (see there for more details).
Let be two groupoids (homotopy 1-types) in ∞Grpd.
A morphism is 0-truncated precisely if it is a faithful functor.
A morphism is 0-connected precisely if it is a full functor and an essentially surjective functor.
Therefore on homotopy 1-types the 0-connected/0-truncated factorization system is the (eso+full, faithful) factorization system.
The general abstract statement is in
A model category-theoretic discussion is in section 8 of
Disucssion in homotopy type theory is in