nLab (n+1,1)-category of n-truncated objects

Idea

Given any object $X$ in any $(k,1)$-category $C$ for a natural number $k$, the $n$-truncated objects of $X$ for $n+1 \lt k$ form an $(n+1,1)$-category, an $(n+1)$-truncated $(k,1)$-category, (though in general it may be a large one, cf. well-powered category). This is called the $(n+1,1)$-category of $n$-truncated objects of $X$, or the $n$-truncated object $(n+1,1)$-category of $X$.

Properties

If $C$ is finitely complete, then the $n$-truncated objects form a finitely complete $(n+1,1)$-category, so we may speak of the finitely complete $(n+1,1)$-category of $n$-truncated objects.

In any coherent $(k,1)$-category, then the $n$-truncated objects form a coherent $(n+1,1)$-category, so we may speak of the coherent $(n+1,1)$-category of $n$-truncated objects.

In any $(k,1)$-topos, the $n$-truncated objects of $X$ form a $(n+1,1)$-topos, so we may speak of the $(n+1,1)$-topos of $n$-truncated objects.

The reader can probably think of other variations on this theme.

If $f : X \to Y$ is a morphism that has pullbacks along $n$-truncated morphisms, then pullback along $f$ induces a $(n+1,1)$-category morphism $f^* : Trunc_n(Y) \to Trunc_n(X)$. This is functorial in the sense that if $g : Y \to Z$ also has this property, then there is an inhabited equivalence $n+1$-groupoid $f^* \circ g^* \cong (g \circ f)^*$.

If $C$ has pullbacks of $n$-truncated morphisms, $Trunc_n$ is often used to denote the contravariant functor $C^{op} \to (n+1,1)Cat$ whose action on morphisms is $Trunc_n(f) = f^*$.

Examples

• A (0,1)-category of (-1)-truncated objects of an object $X$ is a poset of subobjects of $X$.

• A well-pointed Heyting pretopos of 0-truncated objects of the terminal object $1$ is a (possibly) predicative model of the category of sets.

• A well-pointed Heyting Π-pretopos of 0-truncated objects of the terminal object of $1$ is a (possibly) weakly predicative model of the category of sets.

• A well-pointed topos of 0-truncated objects of the terminal object $1$ is an impredicative model of the category of sets.

• A well-pointed W-topos of 0-truncated objects of the terminal object $1$ whose 0-truncated (-1)-connected morphisms all have sections is a model of ETCS.

Related concepts

• If one opts for the alternative definition that $n$-truncated objects are $n$-truncated morphisms into the object (not equivalence large $n+1$-groupoids thereof), then one gets a $(n+1,1)$-precategory of $n$-truncated objects instead. In any case, the $(n+1,1)$-category of $n$-truncated objects $Trunc_n(X)$ in our sense is the $(n+1,1)$-categorical reflection of the $(n+1,1)$-precategory $TruncMor_n(X)$ of $n$-truncated objects in the alternative sense, and of course the reflection Rezk completion map $TruncMor_n(X) \to Trunc_n(X)$ is an equivalence.

• poset of subobjects

• n-truncated object classifier?