homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
A -groupoid or (-2)-type is a (−2)-truncated object in ∞Grpd.
There is, up to equivalence, just one -groupoid, namely the point.
Compare the concepts of -groupoid (a truth value) and -groupoid (a set). Compare also with -category and -poset, which mean the same thing for their own reasons.
The point of -groupoids is that they complete some patterns in the periodic tables and complete the general concept of -groupoid. For example, there should be a -groupoid of -groupoids; a -groupoid is simply a truth value, and is the true truth value.
As a category, is a monoidal category in a unique way, and a groupoid enriched over this should be (at least up to equivalence) a -groupoid, which is a truth value; and indeed, a groupoid enriched over is a groupoid in which any two objects are isomorphic in a unique way, which is equivalent to a truth value.
See (−1)-category for references 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 | (-1)-groupoid/truth value | h-proposition | ||
| h-level 2 | 0-truncated | discrete space | 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 | h-2-groupoid | |
| h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | h-3-groupoid | |
| h-level | -truncated | homotopy n-type | n-groupoid | h--groupoid | |
| h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid |