homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
An -groupoid is an
n-category in which all k-morphisms are equivalences;
In terms of a known notion of (n,r)-category, we can define an -groupoid explicitly as an -category such that:
Or we define an -groupoid abstractly as an n-truncated object in the (∞,1)-category ∞Grpd.
A general model for ∞-groupoids are Kan complexes. In this context an -groupoid in the general sense is modeled by a Kan complex all whose homotopy groups vanish in degree . In this generality one also speaks of a homotopy n-type.
Every such -type is equivalent to a “small” model, an -coskeletal Kan complex: one in which every -sphere for has a unique filler.
Even a bit smaller than this is a Kan complex that is an -hypergroupoid, where in addition to these spheres also the horn fillers in degree are unique.
| 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 |