n-types cover

-types cover


Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

nn-types cover


The property that nn-types cover is a property of a higher category, or an axiom in its corresponding internal logic, which says roughly that every object is covered by one that is truncated at some level.

In a higher category

A higher category is said to satisfy the (external) property that nn-types cover, or to have enough nn-types, if for every object XX there exists an nn-truncated object YY and an effective epimorphism YXY\to X. When n=0n=0 one also says that sets cover or that there are enough sets.

Usually the category in question is some sort of topos or higher topos, or at least a pretopos of an appropriate sort. In this case, the property that nn-types cover means that the subcategory of nn-truncated objects is “generating” in an appropriate sense.

When n=1n=-1, however, having enough nn-types in this sense is not really a useful notion, because (1)(-1)-truncated objects (subterminal objects) are not closed under coproducts. In this case a better condition is that all maps out of subterminal objects are jointly effective epimorphic.


If n>0n\gt 0, then any n-localic (∞,1)-topos has enough (n1)(n-1)-types, since every object is surjected onto by a coproduct of representables which are nn-truncated. The converse seems plausible as well.

A specific example of a higher topos in which sets do not cover is the slice (∞,1)-topos Gpd/B 2\infty Gpd / \mathbf{B}^2 \mathbb{Z} of ∞Grpd over the double delooping of the group of integers, which is equivalently the topos of ∞-actions of the ∞-group (2-group) B\mathbf{B} \mathbb{Z}. From this second perspective, a 1-truncated object of this topos is a groupoid (1-groupoid) together with an automorphism of its identity functor, i.e. an element of its center, and a morphism of such is a functor that respects these central elements. Such an object is 0-truncated if it is essentially discrete, in which case its center is also trivial; thus the 0-truncated objects are just ordinary sets. However, since functors must respect the central elements, there can be no surjective map from a 0-truncated object to a 1-truncated one whose chosen central element is nontrivial.

In homotopy type theory

In homotopy type theory, the (internal) axiom of nn-types cover or enough nn-types says that for any type XX there merely? exists an nn-type YY and a surjection (i.e. a (-1)-connected map) YXY\to X. In symbols:

(X:Type) (Y:nType) (f:YX)surj(f) \prod_{(X:Type)} {\Vert \sum_{(Y:n Type)} \sum_{(f:Y\to X)} surj(f) \Vert }

where \Vert-\Vert denotes the (1)(-1)-truncation. As before, when n=0n=0 we say that sets cover or that there are enough sets.

In models


If an (,1)(\infty,1)-topos satisfies the external property that nn-types cover, then its internal type theory satisfies the internal axiom that nn-types cover.


By the Kripke-Joyal semantics of homotopy type theory, the conclusion requires that for any map XΓX\to \Gamma there is an effective epi p:ΔΓp:\Delta\to \Gamma, an nn-truncated map YΔY\to \Delta, and an effective epi Yp *XY\to p^*X in the slice category over Δ\Delta. Assuming the hypothesis, we can obtain this by letting Δ\Delta be an (external) nn-type cover of Γ\Gamma and YY an (external) nn-type cover of p *Xp^* X.

The converse, however, is not true. For the internal axiom, like all internal statements, is preserved by passage to slices (i.e. introduction of a nonempty context), but we saw above that the slice topos Gpd/B 2\infty Gpd / \mathbf{B}^2 \mathbb{Z} does not have enough sets, even though Gpd\infty Gpd does.

For an example of a topos in whose internal logic sets do not cover, let CC be the (2,1)(2,1)-category with two objects aa and bb, one morphism aba\to b, no morphisms bab\to a, and C(a,a)=BC(a,a) = \mathbf{B} \mathbb{Z} and C(b,b)=1C(b,b)=1, and consider the presheaf (,1)(\infty,1)-topos over CC. A 1-truncated object therein consists of two groupoids X aX_a and X bX_b, an element of the center of X aX_a, and a functor X bX aX_b \to X_a which relates the chosen central element in X aX_a with the identity in the center of X bX_b.

If we take X bX_b to be empty, then X aX_a is a groupoid with an arbitrary chosen central element, and we can choose it to be one which is nontrivial and hence admits no surjection from a 0-type. Let Γ=1\Gamma = 1 for this XX. Since the terminal object 11 is a representable (it is C(,b)C(-,b)), it is projective; thus given Δ\Delta and YY as above, we could find a section of p:ΔΓp:\Delta\to\Gamma and pull back YY along it to obtain a 0-type cover of XX itself, which does not exist.

Relation to other axioms

The internal axiom that sets cover is related to some forms of the axiom of choice. Let us denote by

  • AC 0=AC_0 = every surjection between sets merely has a section.
  • AC =AC_\infty = every surjection with codomain a set merely has a section.

Then we have


AC (AC 0AC_\infty \Leftrightarrow (AC_0 and sets cover).


This is a theorem inside homotopy type theory, and likewise for its proof. Clearly AC AC 0AC_\infty \Rightarrow AC_0. Given XX, we have a map XX 0X\to {\Vert X \Vert_0} which is 0-connected, hence also surjective, and its codomain is a set; thus by AC AC_\infty it merely has a section. Any section of a 0-connected map is surjective; thus XX is merely covered by X 0\Vert X\Vert_0. (Note that in this case we have a stronger version of “sets cover” in which the first \sum is outside the truncation.)

Conversely, suppose AC 0AC_0 and sets cover, and let XZX\to Z be a surjection with codomain a set. Then there merely exists a set YY and a surjection YXY\to X, and the composite surjection YXZY\to X\to Z merely has a section by AC 0AC_0. The composite of this section with YXY\to X is a section of XZX\to Z.

Last revised on May 21, 2018 at 06:27:09. See the history of this page for a list of all contributions to it.