homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
A $(-1)$-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 $(-1)$-groupoids is that they complete some patterns in the periodic table of $n$-categories. (They also shed light on the theory of homotopy groups and n-stuff.)
For example, there should be a $0$-category of $(-1)$-groupoids; a $0$-category is also a set, and this set is the set of truth values: classically
Actually, since for other values of $n$, n-groupoids form not just an $(n+1)$-category but an $(n+1,1)$-category, we should expect the $0$-category of $(-1)$-groupoids to be a $(0,1)$-category, or $1$-poset. This simply means a poset, and indeed truth values do always form a poset, classically ($\bot \leq \top$).
If we equip the category of $(-1)$-groupoids with the monoidal structure of conjunction (the logical AND operation), then a groupoid enriched over this is a setoid, and a category enriched over it is a proset. Up to equivalence of categories, these are the same as a set (a $0$-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 | (-1)-groupoid/truth value | mere proposition, 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 $n+2$ | $n$-truncated | homotopy n-type | n-groupoid | h-$n$-groupoid | |
h-level $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |