Homotopy Hypothesis¶

Assert that homotopy types of spaces and suitably weak infinity-groupoids present equivalent homotopy theories, with paths, homotopies, and all higher homotopies represented as invertible higher morphisms.

Version: v2 · 2026-09-06 · History
Domain-specific #: 2019
Origin domain: mathematics
Subdomain: higher category theory
Aliases: Grothendieck homotopy hypothesis, Infinity-groupoid hypothesis, Homotopy hypothesis for infinity-groupoids

Core Idea¶

The homotopy hypothesis says that spaces viewed only up to homotopy and suitably weak infinity-groupoids encode the same mathematics. A point becomes an object, a path a 1-morphism, a homotopy of paths a 2-morphism, and every higher homotopy a higher morphism; all of these morphisms are invertible at their appropriate level. Grothendieck made this organizing claim central in Pursuing Stacks.^[1]

The slogan “infinity-groupoids are spaces” is not one model-free theorem. A precise result fixes a model of spaces, a definition of weak infinity-groupoid, the relevant weak equivalences, and comparison functors—typically a fundamental infinity-groupoid in one direction and realization in the other—then proves an equivalence of homotopy theories.

Structural Signature¶

A category or higher category of spaces or homotopy types.
A declared model of weak infinity-groupoids.
Objects, paths, and iterated homotopies represented in successive dimensions.
Weak rather than strictly associative and unital higher composition where required.
Invertibility of every positive-dimensional morphism up to coherent higher data.
Weak-equivalence classes on both sides.
A fundamental infinity-groupoid construction from spaces.
A realization or classifying-space construction in the reverse direction.
Unit and counit comparison maps that are weak equivalences.
Equivalence at the level of localized homotopy theories, not literal equality of presentations.
A truncated version relating weak n-groupoids and homotopy n-types.
An explicit settlement claim tied to the chosen model.

What It Is Not¶

It is not the ordinary fundamental group alone, which loses higher homotopy information. It is not merely the homotopy category, which collapses higher mapping structure into sets of homotopy classes. It is not the claim that every strict higher groupoid captures every homotopy type; strictness can remove essential coherence. Nor does a proof for Kan complexes automatically prove the conjecture for Grothendieck's original globular definition.

Scope of Application¶

The hypothesis guides algebraic topology, higher category theory, higher topos theory, derived geometry, and homotopy type theory. Kan complexes provide a standard model in which the space–infinity-groupoid correspondence is built into the established homotopy theory of simplicial sets. Other algebraic or globular models require comparison results of their own. Ara studies the homotopy theory of Grothendieck infinity-groupoids and isolates what is known for that formulation.^[2]

Clarity¶

Every use should state the groupoid model, the space model, the weak equivalences, and whether the claim is an equivalence of categories, homotopy categories, model categories, or infinity-categories. “Proved” is meaningful only after those choices. The n-truncated and untruncated versions should also be separated.

Manages Complexity¶

The hypothesis turns an unbounded tower of geometric deformations into one algebraic-categorical object. Instead of managing points, paths, path homotopies, and all coherences as separate structures, the infinity-groupoid packages them into dimension-indexed composition and invertibility data while preserving the homotopy type.

Abstract Reasoning¶

Choose a category of spaces with weak homotopy equivalences.
Choose a weak infinity-groupoid model.
Define its weak equivalences using homotopy groups or an equivalent criterion.
Construct the fundamental infinity-groupoid functor.
Construct geometric realization or a classifying-space functor.
Compare each space with the realization of its fundamental infinity-groupoid.
Compare each infinity-groupoid with the fundamental object of its realization.
Prove those comparisons are weak equivalences and derive equivalence after localization.

Baez and Dolan place the hypothesis within a broader program relating higher categorical structure and topology.^[3]

Knowledge Transfer¶

The portable pattern is replace a geometric object by a structured representation whose cells record every level of equivalence, then prove the representation loses no information under the declared notion of sameness. The proposed immediate parent is Representation.

Examples¶

An ordinary groupoid models a homotopy 1-type: objects represent points, arrows represent path classes, and higher homotopy groups vanish. A Kan complex can be read as an infinity-groupoid and participates in the standard Quillen equivalence between simplicial sets and topological spaces.^[4]

For an n-type, the proposed categorical representation stops after dimension n. The hard part is not the slogan but choosing weak composition and coherence rich enough to reproduce all such types.

Structural Tensions¶

Geometric continuity versus algebraic composition.
Strict laws versus coherent weak laws.
Presentation-specific objects versus invariant homotopy types.
Truncated dimension versus an infinite coherence tower.
An intuitive slogan versus a model-specific theorem.

Structural–Framed Character¶

Representation across equivalent homotopy theories is structural. Spaces, paths, weak higher categories, groupoidal invertibility, homotopy groups, and realization functors are constitutive. The abstraction is therefore domain-specific.

Structural Core vs. Domain Accent¶

The structural core is object + all equivalences among its parts at every level -> lossless alternate presentation. The domain accent is the equivalence between spaces and weak infinity-groupoids.

Representation is the proposed immediate parent. Isomorphism, Equivalence Relation, Formal System, and Local-to-Global Aggregation are related primes.

The prospective queue contains one strict edge to prime:representation. No live DAG mutation is authorized.

Relationships to Other Abstractions¶

Current abstraction Homotopy Hypothesis Domain-specific

Parents (1) — more general patterns this builds on

Homotopy Hypothesis is a kind of Representation Prime

Representation is the proposed immediate parent.

Hierarchy path (1) — routes to 1 parentless root

Homotopy Hypothesis → Representation → Abstraction

Neighborhood in Abstraction Space¶

Homotopy Hypothesis sits in a sparse region of the domain-specific corpus (79^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Homotopy Category — 0.85
Joyal Model Structure — 0.84
Category of compactly generated weak Hausdorff spaces — 0.82
Whitehead Theorem — 0.82
Stack (Mathematics) — 0.82

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

The fundamental-group functor alone.
The ordinary homotopy category.
The statement that strict infinity-groupoids model every homotopy type.
The Joyal model structure for infinity-categories.
Homotopy type theory's interpretation in spaces, which is connected but not identical.
A proof in one model reported as a model-independent proof of every formulation.

References¶

[1] Alexander Grothendieck, Pursuing Stacks, manuscript (1983), published in Documents Mathématiques 13 (Société Mathématique de France, 2021). registry ↩

[2] Dimitri Ara, “On the Homotopy Theory of Grothendieck Infinity-Groupoids,” Journal of Pure and Applied Algebra 217, no. 7 (2013): 1237–1278, doi:10.1016/j.jpaa.2012.10.010. registry ↩

[3] John C. Baez and James Dolan, “Higher-Dimensional Algebra and Topological Quantum Field Theory,” Journal of Mathematical Physics 36, no. 11 (1995): 6073–6105, doi:10.1063/1.531236. registry ↩

[4] Paul G. Goerss and John F. Jardine, Simplicial Homotopy Theory (Birkhäuser, 1999), doi:10.1007/978-3-0348-8707-6. registry ↩