∞-groupoids
Overview
Higher-dimensional analogues of groupoids: morphisms have morphisms between them. Grothendieck proposed in letters; Voevodsky used for univalent foundations and HoTT.
Era: 1980s–2010s
Proposed at: Princeton, USA / Bures-sur-Yvette, France
Formal structure
Domain: Objects x; 1-morphisms f: x → y; 2-morphisms α: f ⇒ g; …
π_k(x,y) = k-morphisms up to (k+1)-equivalence; composition associative up to higher morphisms
Constraints: All morphisms invertible (up to higher morphisms); Kan complex model
Objective: Univalent foundations; identity = path; types as spaces