homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
The property that -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.
A higher category is said to satisfy the (external) property that -types cover, or to have enough -types, if for every object there exists an -truncated object and an effective epimorphism . When 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 -types cover means that the subcategory of -truncated objects is “generating” in an appropriate sense.
When , however, having enough -types in this sense is not really a useful notion, because -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 , then any n-localic (∞,1)-topos has enough -types, since every object is surjected onto by a coproduct of representables which are -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 of ∞Grpd over the double delooping of the group of integers, which is equivalently the topos of ∞-actions of the ∞-group (2-group) . 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, the (internal) axiom of -types cover or enough -types says that for any type there merely exists an -type and a surjection (i.e. a (-1)-connected map) . In symbols:
where denotes the -truncation. As before, when we say that sets cover or that there are enough sets.
If an -topos satisfies the external property that -types cover, then its internal type theory satisfies the internal axiom that -types cover.
By the Kripke-Joyal semantics of homotopy type theory, the conclusion requires that for any map there is an effective epi , an -truncated map , and an effective epi in the slice category over . Assuming the hypothesis, we can obtain this by letting be an (external) -type cover of and an (external) -type cover of .
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 does not have enough sets, even though does.
For an example of a topos in whose internal logic sets do not cover, let be the -category with two objects and , one morphism , no morphisms , and and , and consider the presheaf -topos over . A 1-truncated object therein consists of two groupoids and , an element of the center of , and a functor which relates the chosen central element in with the identity in the center of .
If we take to be empty, then 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 for this . Since the terminal object is a representable (it is ), it is projective; thus given and as above, we could find a section of and pull back along it to obtain a 0-type cover of itself, which does not exist.
The internal axiom that sets cover is related to some forms of the axiom of choice. Let us denote by
Then we have
and sets cover).
This is a theorem inside homotopy type theory, and likewise for its proof. Clearly . Given , we have a map which is 0-connected, hence also surjective, and its codomain is a set; thus by it merely has a section. Any section of a 0-connected map is surjective; thus is merely covered by . (Note that in this case we have a stronger version of “sets cover” in which the first is outside the truncation.)
Conversely, suppose and sets cover, and let be a surjection with codomain a set. Then there merely exists a set and a surjection , and the composite surjection merely has a section by . The composite of this section with is a section of .
Last revised on April 29, 2023 at 19:26:30. See the history of this page for a list of all contributions to it.