homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
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.
The -groupoids form an (n+1,1)-category, nGrpd.
A general model for ∞-groupoids is provided by Kan complexes (the fibrant objects in the classical model structure on simplicial sets which presents ∞Grpd).
In this context an -groupoid in the general sense is modeled by a Kan complex all of whose homotopy groups vanish in degree . In this generality one also speaks of a homotopy -type or an -truncated object of ∞Grpd.
Every such -type is equivalent to a “small” model, an -coskeletal Kan complex (see there): one in which every -sphere for has a unique filler.
Yet a bit smaller than this are Kan complexes that is an -hypergroupoid, where in addition to these sphere-fillers also the horn fillers in degree are unique.
(For 1-groupoids/1-hypergroupoids this situation is further spelled out here).
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 |
Discussion of homotopy -types/-truncated objects in homotopy type theory:
Univalent Foundations Project, §7 of: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web, pdf]
Nicolai Kraus, Truncation levels in Homotopy Type Theory, Nottingham (2015) [pdf, eprints:28986]
Felix Cherubini, Egbert Rijke, Thm. 3.10 of: Modal Descent, Mathematical Structures in Computer Science , 31 4 (2021) 363-391 [doi:10.1017/S0960129520000201, arXiv:2003.09713]
Last revised on February 14, 2023 at 14:03:55. See the history of this page for a list of all contributions to it.