homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
A -groupoid or (-1)-type is a truth value, or equivalently an (-1)-truncated object in ∞Grpd. By excluded middle, this is either the empty groupoid (false) or the terminal groupoid (true, the point).
Compare the concept of 0-groupoid (a set) and (-2)-groupoid (which is trivial). The point of -groupoids is that they complete some patterns in the periodic table of -categories. (They also shed light on the theory of homotopy groups and n-stuff.)
For example, there should be a -category of -groupoids; a -category is also a set, and this set is the set of truth values: classically
Actually, since for other values of , n-groupoids form not just an -category but an -category, we should expect the -category of -groupoids to be a -category, or -poset. This simply means a poset, and indeed truth values do always form a poset, classically ().
If we equip the category of -groupoids with the monoidal structure of conjunction (the logical AND operation), then a groupoid enriched over this is a symmetric proset, and a category enriched over it is a proset. Up to equivalence of categories, these are the same as a set (a -groupoid) and a poset (a (0,1)-category); this fits the patterns of the periodic table.
See (-1)-category for more on this sort of negative thinking.
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 | -truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h--groupoid |
h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid |
Last revised on September 22, 2022 at 18:55:55. See the history of this page for a list of all contributions to it.