nLab n-truncated object of an (infinity,1)-category

Idea

An $n$-truncated ∞-groupoid is an n-groupoid.

An $n$-truncated topological space is a homotopy n-type: all homotopy groups above degree $n$ are trivial.

An $n$-truncated object in a general (∞,1)-category is an object such that all hom-∞-groupoids into it are $n$-truncated.

If an object in an (∞,1)-topos is $k$-truncated for any (possibly large) $k$, then it is $n$-truncated precisely if all its categorical homotopy groups above degree $n$ are trivial.

The complementary notion of $n$-truncated object is that of an n-connected object of an (∞,1)-category.

Definition

In terms of truncations

Definition

($n$-truncated $\infty$-groupoid)

An ∞-groupoid $A \in \infty Grpd$ is $n$-truncated for $n \in \mathbb{N}$ if it is an n-groupoid:

Precisely: in the model of ∞-groupoids given by Kan complexes $A$ is $n$-truncated if the simplicial homotopy groups $\pi_k(A,x)$ are trivial for all $x$ and all $k \gt n$.

It makes sense for the following to adopt the convention that $A$ is called.

• $(-1)$-truncated if it is empty or contractible – this is a (-1)-groupoid.

• $(-2)$-truncated if it is non-empty and contractible – this is a (-2)-groupoid.

(following HTT, p. 6).

To generalize this, let now $C$ be an arbitrary (∞,1)-category. For $X,A$ objects in $C$ write $C(X,A) \in$ ∞Grpd for the (∞,1)-categorical hom-space (if $C$ is given as a simplicially enriched category then this is just the SSet-hom-object which is guaranteed to be a Kan complex).

Using this, it is useful to reformulate the above as follows slightly:

Lemma

An ∞-groupoid $A$ is $n$-truncated precisely when for all ∞-groupoids $X$ the hom-$\infty$-groupoid $\infty Grpd(X,A)$ is $n$-truncated.

In other category-theoretic terms this says that (∞,k)-transformation between $X$ and $A$, whose components are k-morphisms in $A$, cannot be nontrivial for $k \gt n$ if there are no nontrivial k-morphisms with $k \gt n$ in $A$.

Using this fact we can transport the notion of $n$-truncation to any (∞,1)-category by testing it on hom-$\infty$-groupoids:

Definition

($n$-truncated object in an $(\infty,1)$-category)

Given an (∞,1)-category $\mathcal{C}$, an object $A \in \mathcal{C}$ is called $n$-truncated, for $n \in \mathbb{N}$, if for all objects $X \in \mathcal{C}$ the hom-∞-groupoid $\mathcal{C}(X,A)$ is $n$-truncated according to Def. .

This is HTT, def. 5.5.6.1.

Some terminology:

• A 0-truncated object is also called discrete. Notice that this is categorically discrete as in discrete category, not discrete in the sense of discrete topological space. An object in an (∞,1)-topos is discrete in this sense if, regarded as an ∞-groupoid with extra structure, it has only trivial morphisms.

• By the above convention on (-2)-truncated $\infty$-groupoids, it is only the terminal objects of $C$ that are (-2)-truncated.

• Similarly, the (-1)-truncated objects are the subterminal objects.

Definition

($n$-truncated morphism in an $(\infty,1)$-category)

A morphism $f : X \to Y$ of ∞-groupoids is $n$-truncated if all of its homotopy fibers are $n$-truncated by def. .

A morphism $f : X \to Y$ in an (∞,1)-category $C$ is $n$-truncated if for all $W \in C$ the postcomposition morphism

$$C(W,f) : C(W,X) \to C(W,Y)$$

is $n$-truncated in ∞Grpd.

This is HTT, def. 5.5.6.8.

By the characterization of homotopy fiber of functor categories this is equivalent to saying that $f$ is $k$-truncated when it is so regarded as an object of the over (∞,1)-category $C_{/Y}$. (See also HTT, rem. 5.5.6.12.)

Unwinding the definitions and applying the long exact sequence of homotopy groups, we have:

Proposition

For $n \geq -1$, a morphism $f : X \to Y$ of ∞-groupoids is $n$-truncated iff, for every point $x \in X$, we have $\pi_{n+1}(X, x) \to \pi_{n+1}(Y, f(x))$ is a monomorphism and for every $k \geq n+2$, $\pi_k(X, x) \to \pi_k(Y, f(x))$ is an isomorphism.

$f$ is $(-2)$-trunacated iff it is a weak homotopy equivalence.

In terms of categorical homotopy groups

At least if the ambient (∞,1)-category is even an ∞-stack (∞,1)-topos there is an alternative, more intrinsic, characterization of $n$-truncation in terms of categorical homotopy groups in an (∞,1)-topos:

Proposition

Suppose that an object $X$ in an ∞-stack (∞,1)-topos is $k$-truncated for some $k \in \mathbb{N}$ (possibly very large).

Then for any $n \in \mathbb{N}$ this $X$ is $n$-truncated precisely if all the categorical homotopy groups above degree $n$ are trivial.

Proof

This is HTT, prop 6.5.1.7.

Remark

Notice that this expected statement does require the assumption that $X$ is $k$-truncated for some $k$. Without any a priori truncation assumption on $X$, there is no comparable statement about the relation to categorical homotopy groups. See HTT, remark 6.5.1.8.

Properties

Recursive definition

Proposition

In an $(\infty,1)$-category $C$ with finite limits, a morphism $f : X \to Y$ is $k$-truncated (for $k \geq -1$) precisely if the diagonal morphism $X \to X \times_Y X$ is $(k-1)$-truncated.

This is HTT, lemma 5.5.6.15.

Proof

By definition $f$ is $k$-truncated if for each object $d \in C$ we have that $C(d,f)$ is $k$-truncated in ∞Grpd. Since the hom-functors $C(d,-)$ preserve (∞,1)-limits, we have in particular that $X \to X \times_Y X$ in $C$ is $k$-truncated if $C(d,X) \to C(d,X) \times_{C(d,Y)} C(d,X)$ is $k$-truncated for all $d$ in ∞Grpd. Therefore it is sufficient to prove the statement for morphisms in $C =$ ∞Grpd.

So let now $f : X \to Y$ be a morphism of ∞-groupoids. We may find a fibration $\bar \phi : \bar X \to \bar Y$ between Kan complexes in sSet that models $f : X \to Y$ in the standard model structure on simplicial sets, and by the standard rules for homotopy pullbacks it follows that the object $X \times_Y X$ in $\infty$-Grpd is then modeled by the ordinary pullback $\bar X \times_{\bar Y} \bar X$ in sSet. And the homotopy fibers of $f$ over $y \in Y$ are then given by the ordinary fibers $\bar X_y$ of $\bar f$ in $sSet$.

This way, the statement is reduced to the following fact: a Kan complex $\bar X_y$ is $k$-truncated precisely if the homotopy fibers of $\bar X_y \to \bar X_y \times \bar X_y$ are $(k-1)$-truncated.

We now write $X$ for $\bar X_y$ for simplicity. To see the last statement, let $(a,b) : * \to X \times X$ and compute the homotopy pullback

$$\array{ Q &\to& * \\ \downarrow && \downarrow^{\mathrlap{(a,b)}} \\ X &\to& X \times X }$$

as usual by replacing the right vertical morphism with the fibration $(X \times X)^I \times_{X \times X} (a,b) \to X \times X$ and then forming the ordinary pullback. This shows that $Q$ is equivalent to the space of paths $P_{a,b}X$ in $X$ from $a$ to $b$. (Use that gluing of path space objects at endpoints of paths produces a new path space; see, for instance, section 4 of BrownAHT).

If $X$ is connected, then choosing any path $a \to b$ gives an isomorphism from the homotopy groups of $P_{a,b} X$ to those of the loop space $\Omega_a X$. These latter are indeed those of $X$, shifted down in degree by one (as described, for instance, at fiber sequence).

If $X$ is not connected, we can easily reduce to the case that it is.

General

Proposition

For $C$ an $(\infty,1)$-category and $k \geq -2$, the full sub-(∞,1)-category $\tau_{\leq k} C$ is stable under all $\infty$-limits in $C$.

This is HTT, prop. 5.5.6.5.

Proposition

Let $\mathbf{H}$ be an (∞,1)-topos. For all $(-2) \leq n \lt \infty$ the class of $n$-truncated morphisms in $\mathbf{H}$ forms the right class in a orthogonal factorization system in an (∞,1)-category. The left class is that of n-connected morphisms in $\mathbf{H}$.

This appears as a remark in HTT, Example 5.2.8.16. A construction of the factorization in terms of a model category presentation is in (Rezk, prop. 8.5). See also n-connected/n-truncated factorization system.

Model category presentations

There are model structures for homotopy n-types that presentable (∞,1)-category present the full sub-(∞,1)-categories of $n$-truncated objects in some ambient $(\infty,1)$-category. See there for more details.

Truncation

Definition

Under mild conditions there is for each $n$ a universal way to send an arbitrary object $A$ to its $n$-truncation $\tau_{\leq n} A$. This is a general version of decategorification where n-morphisms are identified if they are connected by an invertible $(n+1)$-morphism.

For $C$ an (∞,1)-category and $n \geq -2$ in $\mathbb{Z}$ write $\tau_{\leq n} C$ for the full subcategory of $C$ on its $n$-truncated objects.

So for instance for $C =$ ∞Grpd we have $\tau_{\leq n} \infty Grpd = n Grpd$.

Proposition

If $C$ is an (∞,1)-category that is presentable then the canonical inclusion (∞,1)-functor

$$\tau_{\leq n} C \hookrightarrow C$$

has an accessible left adjoint

$$\tau_{\leq n} : C \to \tau_{\leq n} C \,.$$

This is HTT 5.5.6.18.

Indeed, as the notation suggests, $\tau_{\leq n} C$ is the essential image of $C$ under $\tau_{\leq n}$. The image $\tau_{\leq n} A$ of an object $A$ under this operation is the $n$-truncation of $A$.

So $n$-truncated objects form a reflective sub-(∞,1)-category

$$\tau_{\leq n} C \stackrel{\overset{\tau_{\leq n}}{\leftarrow}}{\hookrightarrow} C \,.$$

Properties

General

Proposition

For any small $\infty$-category $C$, $\tau_{\leq n} PSh(C, \infty Grpd) \simeq PSh(C, n Grpd)$, and truncation acts pointwise.

Proof

If $P$ is an $n$-truncated ∞-presheaf, then $P(c) \simeq PSh(C)(C(-, c), P)$ is $n$-truncated; thus $P$ takes values in $n Grpd$.

Conversely, if $P$ takes values in $n Grpd$, then the fact every presheaf is a colimit of representables implies $hom(Q, P)$ is a limit of $n$-truncated spaces and is thus $n$-truncated.

Given this identification of the subcategory of $n$-truncated objects, we can see that the truncation-inclusion adjunction between $n Grpd$ and $\infty Grpd$ induces an adjunction whose right adjoint is the inclusion $PSh(C, n Grpd) \to PSh(C, \infty Grpd)$

Corollary

(left exact $\infty$-functors preserve truncation)
A left exact $\infty$-functor $F \colon C \to D$ between $(\infty,1)$-categories with finite $\infty$-limits sends $k$-truncated objects/morphisms to $k$-truncated objects/morphisms.

(HTT, prop. 5.5.6.16)

Proof

This follows from the above recursive characterization of $k$-truncated morphisms by the $(k-1)$-truncation of their diagonal, which is preserved by the finite limit preserving $F$.

Proposition

A left exact presentable $(\infty,1)$-functor $F : C \to D$ between locally presentable (∞,1)-categories $C$ and $D$ commutes with truncation:

$$F \circ \tau^C_{\leq k} \simeq \tau^D_{\leq k} \circ F \,.$$

This is HTT, prop. 5.5.6.28.

Proof

By the above lemma, $F$ restricts to a functor on the truncations. So we need to show that the diagram

$$\array{ C &\stackrel{F}{\to}& D \\ {}^{\mathllap{\tau_{\leq k}}}\downarrow & (?) & \downarrow^{\mathrlap{\tau_{\leq k}}} \\ \tau_{\leq k } C &\stackrel{F}{\to}& \tau_{\leq k} D }$$

in (∞,1)Cat can be filled by a 2-cell. To see this, notice that the adjoint (∞,1)-functor of both composite morphisms exists (because that of $F$ exists by the adjoint (∞,1)-functor theorem and bcause adjoints of composites are composites of adjoints) and since the bottom morphism is just the restriction of the top morphism and the right adjoints of the vertical morphisms are full inclusions this adjoint diagram

$$\array{ C &\stackrel{G}{\leftarrow}& D \\ \uparrow & & \uparrow \\ \tau_{\leq k } C &\stackrel{G}{\leftarrow}& \tau_{\leq k} D } \,.$$

evidently commutes since it just expresses this restriction.

Proposition

If $C$ is an (∞,1)-topos, then truncation $\tau_{\leq n} : C \to C$ preserves finite products.

This appears as HTT, lemma 6.5.1.2.

Proof

First notice that the statement is true for $C =$ ∞Grpd. For instance we can use the example In ∞Grpd and Top, model ∞-groupoids by Kan complexes and notice that then $\tau_{\leq n}$ is given by the truncation functor $tr_{n+1} : sSet \to [\Delta^{op}_{\leq n+1}, Set]$. This is also a right adjoint and as such preserves in particular products in $sSet$, which are $(\infty,1)$-products in $\infty Grpd$.

From that we deduce that the statement is true for $C$ any (∞,1)-category of (∞,1)-presheaves $C = PSh_{(\infty,1)}(K) = Func_{(\infty,1)}(K^{op}, \infty Grpd)$ because all relevant operations there are objectwise those in $\infty Grpd$.

So far, this shows even that on presheaf $(\infty,1)$-toposes, all products (not necessarily finite) are preserved by truncation.

A general (∞,1)-topos $C$ is (by definition) a left exact reflective sub-(∞,1)-category of a presheaf $(\infty,1)$-topos,

$$C \stackrel{\overset{L}{\leftarrow}}{\underset{i}{\hookrightarrow}} PSh_{(\infty,1)}(K) \,.$$

Let $\prod_{j} i(X_j)$ be the product of the objects in question taken in $PSh(K)$. By the above there, we have an equivalence

$$\tau_{\leq k} \prod_j i(X_j) \stackrel{\simeq}{\to} \prod_j \tau_{\leq} i(X_j) \,.$$

Now applying $L$ to this equivalence and using now that $L$ preserves the finite product, this gives an equivalence

$$L \tau_{\leq k} \prod_j i(X_j) \stackrel{\simeq}{\to} L \prod_j \tau_{\leq k} i(X_j) \simeq \prod_j L \tau_{\leq k} i(X_j)$$

in $C$. The claim follows now with the above result that $L \circ \tau_{\leq n} \simeq \tau_{\leq n} \circ L$.

Postnikov tower

By the fact that the truncation functor $\tau_{\leq n}$ is a left adjoint, one obtains canonical morphisms

$$A \to \tau_{\leq n}A$$

as the adjunct of the identity on $A$, and then by iteration also canonical morphisms

$$\tau_{\leq (n+1)} A \to \tau_{\leq n} A \,.$$

For any $A \in C$, the sequence

$$\cdots \to \tau_{\leq 2}A \to \tau_{\leq 1} A \to \tau_{\leq 0} A$$

is the Postnikov tower in an (∞,1)-category of $A$. See there for more details.

Homotopy type theory syntax

Discussion of $n$-truncation of types in homotopy type theory via higher inductive types is in (Brunerie). This sends a type to an h-level $(n+2)$-type. The $(-1)$-truncation in the context is forming the bracket type hProp.

See at n-truncation modality.

Relation to homotopy groups

In an $(\infty,1)$-topos $C$ there is a notion of categorical homotopy groups in an (∞,1)-topos. For the $(\infty,1)$-topos ∞Grpd given by the model of Kan complexes this coincides with the notion of simplicial homotopy groups:

Observation

An object $A$ in the (∞,1)-topos ∞Grpd is $n$-truncated precisely if its categorical homotopy groups $\pi_k(A)$ vanish for all $k \gt n$.

This simple relation between $n$-truncation and categorical homotopy groups is almost, but not exactly, true in an arbitrary (∞,1)-topos.

Proposition

Let $\mathbf{H}$ be an (∞,1)-topos and $A \in \mathbf{H}$ an $n$-truncated object.

Then

1. for $k \gt n$ we have for the categorical homotopy groups $\pi_k(A) = *$;

2. if (for $n \geq 0$) $\pi_n(A) = *$, then $X$ is in fact $(n-1)$-truncated.

This implies

Corollary

If $A \in \mathbf{H}$ is truncated at all (for any value), then it is $n$-truncated precisely if all categorical homotopy groups vanish $\pi_k(A) = *$ for $k \gt n$.

Notice. If $A$, on the other hand, is not truncated at all, then all its homotopy groups may be trivial, and $A$ may still not be equivalent to the terminal object. This means that Whitehead's theorem may fail in a general (∞,1)-topos for untruncated objects. It holds, however, in hypercomplete (∞,1)-toposes.

Examples

Truncated morphisms

General

A morphism $f : X \to 0$ is

• (-2)-truncated precisely if it is an equivalence;

• (-1)-truncated precisely if it is a monomorphism.

Between groupoids

For morphisms between 1-groupoids, the notion of $n$-truncation for low $n$ reproduces standard concepts from ordinary category theory.

Proposition

A functor $f : X \to Y$ between groupoids, is $n$-truncated precisely when regarded as a morphism in ∞Grpd it is

• for $n = -2$ – an equivalence of categories;

• for $n = -1$ – a full and faithful functor;

• for $n = 0$ – a faithful functor.

Proof

Notice that $f$ being faithful means precisely that it induces a monomorphism on the first homotopy groups.

For $x : * \to X$ any point and $F_{f(x)}$ the corresponding homotopy fiber of $f$, the long exact sequence of homotopy groups gives that $\pi_1(F)$ is the kernel of an injective map

$$\cdots \to \pi_1(F) \to \pi_1(X) \hookrightarrow \pi_1(Y,f(x)) \to \cdots \,,$$

hence $\pi_1(F_{y}) = *$ for all points $y$ in the essential image of $f$. For $y$ not in the essential image we have $F_y \simeq \emptyset$. In either case, it follows that $F$ is 0-truncated.

By def. this is the defining condition for $f$ to be 0-truncated.

Between stacks

Let $C$ be a site and write $Sh_{(2,1)}(C) \hookrightarrow Sh_{(\infty,1)}(C)$ for the (2,1)-topos of stacks/(2,1)-sheaves inside the (∞,1)-sheaf (∞,1)-topos of all ∞-stacks/(∞,1)-sheaves.

Write $L_W [C^{op}, Grpd]$ for the simplicial localization of groupoid valued presheaves in $C$ and write $[C^{op}, sSet]_{proj,loc}$ for the local projective model structure on simplicial presheaves that presents $Sh_{(\infty,1)}(C)$.

Proposition

Let $f : X \to Y$ be a morphism of stacks that has a presentation by a degreewise faithful functor that, under the nerve, goes between fibrant simplicial presheaves.

Then $f$ is 0-truncated as a morphism in $Sh_{(\infty,1)}(C)$.

Proof

We need to check that for any $\infty$-stack $A$, the morphism $Sh_\infty(A,f)$ is 0-truncated in ∞Grpd. We may choose a cofibrant model for $A$ in $[C^{op}, sSet]_{proj,loc}$ and by assumption that $X$ and $Y$ is fibrant we have that the ordinary hom of simplicial presheaves $[C^{op}, sSet](A, f)$ is the correct derived hom space morphism. This is itself (the nerve of) a faithful functor, hence the statement follows with prop. .

In $\infty Grpd$ and in $Top$

An object in ∞Grpd is $n$-truncated precisely if it is an n-groupoid. To some extent, this is so by definition. Equivalently, an object in Top is $n$-truncated if it is (in the equivalence class of) a homotopy n-type.

So we have for $n \in \mathbb{N}$ a reflective sub-(∞,1)-category

$$n Grpd \stackrel{\overset{\tau_{\leq n}}{\leftarrow}}{\hookrightarrow} \infty Grpd \,.$$

Observation

If we model the (∞,1)-category ∞Grpd as the Kan complex-enriched category/fibrant simplicial category $KanCplx \subset$ sSet of Kan complexes, then the truncation adjunction

$$(\tau_{\leq n } \dashv i) : n Grpd \stackrel{\overset{\tau_{\leq n}}{\leftarrow}}{\hookrightarrow} \infty Grpd \,.$$

is modeled by the simplicial coskeleton sSet-enriched adjunction

$$(tr_{n+1} \dashv cosk_{n+1}) : KanCplx_{n+1} \stackrel{\overset{tr_{n+1}}{\leftarrow}}{\underset{cosk_{n+1}}{\to}} KanCplx \,,$$

where $KanCplx_{n+1}$ is the subcategory of $[\Delta^{op}_{\leq n+1}, Set]$ on those truncated simplicial sets that are truncations of Kan complexes, regarded as a Kan-complex-enriched category by the embedding via $cosk_{n+1}$.

Proof

Notice that every Kan complex $X$ which is $n$-truncated is homotopy equivalent to one in the image of $cosk_{n+1}$, namely to $cosk_{n+1} tr_{n+1} X$, because by one of the properties of $cosk_{n+1}$ we have that the unit

$$X \to cosk_{n+1} tr_{n+1} X$$

induces isomorphisms on homotopy groups $\pi_k$ for $k \leq n$.

This shows that $KanCplx_{n+1}$ is indeed a full sub-(∞,1)-category of $KanCplx$ on $n$-truncated objects

Moreover, by the fact discussed at Simplicial and derived adjunctions at adjoint (∞,1)-functor we have that the sSet-enriched adjunction $(tr_{n+1} \dashv cosk_{n+1})$ on $KanCplx$ indeed presents a pair of adjoint (∞,1)-functors on ∞Grpd. So $tr_{n+1} : KanCplx \to KanCplx$ indeed presents the left adjoint $\tau_{\leq} : \infty Grpd \to n Grpd$ to the inclusion $n Grpd \hookrightarrow \infty Grpd$.

Diagonals

Example

In ordinary category theory we have that a morphism is a monomorphism (as discussed there), precisely if its diagonal is an isomorphism. Embedded into (∞,1)-category, this becomes the special case of prop. for $n = 0$: a morphism is (-1)-truncated (hence a monomorphism in an (∞,1)-category), precisely if its diagonal is (-2)-truncated (hence an equivalence in an (∞,1)-category).

Example

Let $X$ be an object that is $n$-truncated. This means that $X \to *$ is an $n$-truncated morphism. So by prop. the diagonal on that object

$$\Delta : X \to X \times X$$

is an $(n-1)$-truncated morphism, and precisely if it is $(n-1)$-truncated is $X$ $n$-truncated.

In particular, the diagonal is a monomorphism in an (∞,1)-category, hence (-1)-truncated, precisely if $X$ is $0$-truncated (an h-set).

Related concepts

• n-truncation modality

• $n$-truncated morphism / n-connected morphism

• n-groupoid, homotopy n-type

• model structure for homotopy n-types

homotopy level	n-truncation	homotopy theory	higher category theory	higher topos theory	homotopy type theory
h-level 0	(-2)-truncated	contractible space	(-2)-groupoid		true/​unit type/​contractible type
h-level 1	(-1)-truncated	contractible-if-inhabited	(-1)-groupoid/​truth value	(0,1)-sheaf/​ideal	mere proposition/​h-proposition
h-level 2	0-truncated	homotopy 0-type	0-groupoid/​set	sheaf	h-set
h-level 3	1-truncated	homotopy 1-type	1-groupoid/​groupoid	(2,1)-sheaf/​stack	h-groupoid
h-level 4	2-truncated	homotopy 2-type	2-groupoid	(3,1)-sheaf/​2-stack	h-2-groupoid
h-level 5	3-truncated	homotopy 3-type	3-groupoid	(4,1)-sheaf/​3-stack	h-3-groupoid
h-level $n+2$	$n$-truncated	homotopy n-type	n-groupoid	(n+1,1)-sheaf/​n-stack	h-$n$-groupoid
h-level $\infty$	untruncated	homotopy type	∞-groupoid	(∞,1)-sheaf/​∞-stack	h-$\infty$-groupoid

References

In $\infty$-category theory

Discussion in $(\infty,1)$-category:

• Jacob Lurie, Section 5.5.6 of: Higher Topos Theory

Discussion of categorical homotopy groups in an (∞,1)-topos is in section 6.5.1 there.

Discussion in terms of model category presentations:

• Charles Rezk, Section 7 of: Toposes and homotopy toposes, 2010 (pdf, pdf)

A classical article that amplifies the expression of Postnikov towers in sSet (hence in $Grpd_{\infty}$) in terms of coskeleta:

• William Dwyer, Dan Kan, An obstruction theory for diagrams of simplicial sets (pdf)

Discussion in the context of modal homotopy type theory:

• Univalent Foundations Project, section 7.6 of Homotopy Type Theory – Univalent Foundations of Mathematics

• Guillaume Brunerie, Truncations and truncated higher inductive types (web)

More discussion of the internal perspective:

• Nima Rasekh, An Elementary Approach to Truncations (arXiv:1812.10527)

In homotopy type theory

Discussion of homotopy $n$-types/$n$-truncated objects in homotopy type theory:

• Univalent Foundations Project, §7 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]

• Nicolai Kraus, Truncation levels in Homotopy Type Theory, Nottingham (2015) [pdf, eprints:28986]

• Felix Cherubini, Egbert Rijke, Thm. 3.10 of: Modal Descent, Mathematical Structures in Computer Science , 31 4 (2021) 363-391 [doi:10.1017/S0960129520000201, arXiv:2003.09713]