The homotopy hypothesis: elementary expansions and partial cylinders

Source and verification

This article explains family 312 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ From paths and higher homotopies to spaces

Paths can be composed, reversed and deformed, but these operations usually satisfy their identities only up to further homotopy. Grothendieck’s homotopy hypothesis asks whether an algebraic system retaining all those weak coherences recovers the homotopy theory of spaces.

Family 312 claims this result for every Grothendieck coherator in the specified Ara–Henry convention. Its main new theorem is an elementary-expansion assertion: freely adjoining a parallel cell and a homotopy connecting it to an existing cell does not change homotopy groups. The comparison with spaces then uses Henry’s established machinery. (OpenAI, 2026)

The scope of the algebraic model matters. Weak globular infinity-groupoids carry higher coherence operations. Replacing them by strict globular infinity-groupoids is not innocuous: under realizations preserving homotopy groups, the simply connected strict models represent only products of Eilenberg–Mac Lane spaces. The claim here concerns the weak models of the chosen coherator.

🏷️ Preliminaries: globes, operations and free models

A globular set has cells in dimensions $0,1,2,\dots$, with source and target maps. A one-cell is an arrow between vertices, a two-cell goes between parallel arrows, and so on. Two positive-dimensional cells are parallel when their immediate sources and targets agree; any two vertices count as parallel.

The $j$-globe $d_j$ is the basic shape of one $j$-cell with its faces. A finite globular pasting scheme glues such shapes along matching source and target faces. Its height is its largest cell dimension.

A coherator specifies composition and coherence operations by a chosen sequence of free adjunctions. At each stage it adds fillers for specified parallel operations. In the convention used by this manuscript, a generating filler of output dimension $j$ has a pasting-scheme arity of height at most $j$. Every admissible parallel pair eventually has a filler.

This height condition applies to the generators. Composite operations of small output dimension can have larger arities. The proof therefore interprets operations in their original free-adjunction order, rather than sorting them by output dimension. Independently chosen fillers are not identified by additional equations; their prescribed faces and the consequences of functoriality determine the model structure.

Fix a coherator $\mathcal{C}$. A model is a globular set equipped with its operations, respecting the specified faces. Let $F$ be the free-model functor and put

$$D_j=F(d_j),\partial D_j=F(\partial d_j).$$

The notation $D_j$ denotes a free algebraic model, so it includes all composites and coherence cells generated by the basic globe. A map $D_j\to X$ specifies any $j$-cell of $X$, including a composite.

The two families of attachments are

$$\begin{array}{c}{I}_j:\partial D_j\to D_j,\\ J_j:D_j\stackrel{s}{\to }{D}_{j+1}.\end{array}$$

An $I_j$-attachment adds a cell with prescribed boundary. A $J_j$-attachment first adds a parallel $j$-cell and then a joining $(j+1)$-cell. A model is cellular if it is built from the initial model by a possibly transfinite sequence of boundary attachments. The zero-dimensional boundary is empty, so adjoining vertices is included.

🏷️ The elementary-expansion theorem

Manuscript claim

For any cellular model $X$, any $n\ge 0$ and any cell $a:D_n\to X$, the canonical map

$$\begin{array}{c}i:X⟶X^{+},\\ X^{+}=X{⨿}_{D_n}{D}_{n+1},\end{array}$$

formed along the source inclusion, induces a bijection on components and isomorphisms on every based homotopy group.

For $n=0$, this adds a new vertex and an arrow from the selected vertex to it. In higher dimensions it adds a parallel cell and a homotopy from the selected one to the new one.

There is an evident retraction $r:X^{+}\to X$: send the new parallel cell to $a$ and the joining cell to its unit homotopy. But $ri=\mathrm{id}$ only gives a split inclusion. The free extension also generates many composites and coherences involving the new cell. The proof must control their homotopy classes, not just the two visibly attached generators.

An exact-boundary test

The manuscript uses an equivalent criterion for weak equivalence. Given any specified boundary $b:\partial D_k\to X$ and a target $k$-cell $y$ with boundary $fb$, one must find a source cell $x$ with boundary exactly $b$, together with a $(k+1)$-cell joining $f(x)$ to $y$.

This single lifting-up-to-homotopy condition includes both surjectivity and injectivity. To reflect a homotopy between two source cells, apply the criterion one dimension higher to their prescribed boundary and the target joining cell. At dimension zero it supplies the component test.

Finite boundaries, disks and witnesses imply closure under filtered colimits. No injectivity of the transition maps is needed. Together with two-out-of-three and retract closure, this supplies the homotopical tools before any model structure has been constructed.

🏷️ Finite cutoffs and the order of induction

Fix $q\ge 0$. A model is $q$-coskeletal here if every boundary in dimension greater than $q$ has exactly one filler. Distinct parallel $q$-cells are retained; their joining $(q+1)$-cell becomes unique.

The manuscript constructs a reflector $R_q$ to these models that preserves every cell through dimension $q$. It retains the lower globular set and adds unique higher fillers, interpreting each generating operation in the original coherator order. The generator arity bound ensures that an operation of output dimension at most $q$ uses only retained input cells. Higher operations use the unique filler of their already interpreted boundary.

As a left adjoint, $R_q$ preserves the actual algebraic pushouts and cellular presentations. Reflecting a boundary attachment above dimension $k$ into the $k$-coskeletal category makes it an isomorphism. Since the reflection unit preserves lower cells, such an attachment was already bijective on cells through $k$ in the original category.

At fixed $q$, prove the expansion assertion by descending induction on $n$. The case $n=q$ follows from the elementary retraction and unique higher fillers. For the step at $n<q$, only expansions $J_j$ with $j>n$ are already available.

There are three distinct orders in the construction:

Construction	Order used
Expansion theorem at a fixed cutoff	Descending expansion index $n$
Cylinder objects inside one step	Increasing cell dimension $j$
Operations on the resulting path model	Original free stage order of $\mathcal{C}$

Keeping them separate prevents a circular use of the expansion currently being proved.

A consequence for upper attachments

Call an attachment upper if its index is greater than $n$. The induction hypotheses imply that an upper $J$-cellular extension from a cellular object is a weak equivalence.

Now suppose an upper $I$-cellular map is already known to be a weak equivalence. Factor it, by the ordinary small-object construction, into upper $J$-attachments followed by a map lifting those $J_j$. Two-out-of-three makes the latter a weak equivalence. The exact-boundary criterion first gives an approximate lift; lifting its joining homotopy then corrects it to a strict boundary lift.

The original upper $I$-map is consequently a retract of an upper $J$-extension. It has a retraction, and its pushout along a map to a cellular object is again a weak equivalence. These are precisely the pushouts needed later. The argument does not assume a general pushout theorem for all weak equivalences.

🏷️ Turning generator homotopies into a result for the whole model

A model is contractible if it is nonempty and every parallel pair of cells admits a joining cell; equivalently, it has one component and trivial based homotopy groups. Free models on globular pasting schemes are contractible. The source proves this using a finite spine: to compare parallel $m$-cells, retain a pasting scheme of height at most $m+1$ that preserves all cells through $m$. The coherator’s filler property now applies at that bounded arity. This result is obtained before the elementary-expansion induction.

The next objects are finite oriented trees whose vertices are parallel $n$-cells and whose edges are $(n+1)$-cells, with common lower boundary. They are generally not pasting schemes. Replace each tree by a linear string on the same labelled vertices. Paths and inverse paths define maps between their free models

$$A\stackrel{f}{\to }L\stackrel{g}{\to }A,$$

where $L$ is contractible. On each generating edge $e$, cancellation of backtracking in the original tree gives a homotopy $e\to gf(e)$ of dimension $n+2$.

Individual edge homotopies do not yet give a homotopy-compatible statement about every freely generated operation. The manuscript adjoins a duplicate $e^{\prime }$ and a joining cell $e\to e^{\prime }$ for each edge. These are $J_{n+1}$-attachments, covered by the higher-index induction. Call the enlarged model $Q$.

The original and duplicate maps $a_0,a_1:A\to Q$ have a common retraction. Since $a_0$ is a weak equivalence, two-out-of-three makes both that retraction and $a_1$ weak equivalences. Freeness extends the chosen edge homotopies to a model map $h:Q\to A$ satisfying

$$h{a}_0={\mathrm{id}}_A,h{a}_1=gf.$$

It follows that $gf$ is a weak equivalence. Since it factors through the contractible $L$, the components and based homotopy groups of $A$ are trivial. This is the crucial promotion from homotopies on generators to control of the whole algebraic model, using $J_{n+1}$ and never the unproved $J_n$ case.

🏷️ Partial cylinders and compatible operations

The path construction is tailored to the current expansion index $n$. A cylinder leaves all dimensions below $n$ stationary; at dimension $n$ it is a single joining $(n+1)$-cell. In higher dimensions it includes fillers making these movements compatible along shared faces.

Let $P_j$ represent a cylinder on a $j$-cell, so its cells in a target $Y$ are maps $P_j\to Y$. Set $P_j=D_j$ for $j<n$ and $P_n=D_{n+1}$. For higher $j$, start from the boundary-cylinder data with both endpoint disks prescribed, and attach upper cells until all required upper boundaries fill. These completions can be infinite; finite cellularity of $P_j$ is not asserted.

There are two different prescribed-data objects. The one-sided object $A_j^{ϵ}$ fixes the boundary cylinder and one endpoint. The two-sided object $A_j^{01}$ fixes the boundary cylinder and both endpoints. They play different roles: one-sided retractions will give endpoint lifting, while the two-sided object controls interpretation of operations with both endpoint values fixed.

For a pasting scheme $S$, glue the $P_j$ along its actual cells and shared faces to obtain $P(S)$. The exact skeletal formula starts with the original free shape with whiskers on its $n$-cells, then successively pushes out

$$A_{\ell }^{ϵ}⟶P_{\ell }(\ell >n).$$

Shared faces use the same previous-skeleton map; no extra copy is introduced. Tree contractibility handles the initial whiskered shape. Increasing induction on $j$, together with the upper-attachment lemma, then proves contractibility of $P(S)$ and the one-sided objects. Each one-sided map has a retraction.

Choosing operations naturally

Define $(\mathcal{P}Y{)}_j=\mathrm{Hom}(P_j,Y)$ through the cutoff. Its endpoint maps initially form maps of globular sets. To make them maps of the full algebraic models, interpret every coherator generator in its original stage order.

For a generator with arity $S$, all its face operations are already interpreted. Yoneda represents those natural face operations by maps into $P(S)$. Together with the two prescribed endpoint values they define a map

$$A_j^{01}⟶P(S).$$

Contractibility of $P(S)$ extends it across the cellular map to $P_j$. Choose this representing extension once. Precomposition defines the operation on cylinders, and postcomposition by any $Y\to Z$ automatically respects it. This produces a functor $\mathcal{P}$ and natural endpoint model maps, rather than object-by-object choices lacking naturality.

Each endpoint $p_{ϵ}:\mathcal{P}Y\to Y$ lifts every boundary inclusion, using the one-sided retractions. The joint endpoint map lifts the particular source inclusion $J_n$. Its prescribed data form a four-vertex tree

$$y_0-x_0-x_1-y_1,$$

with edges given by the source cylinder and the two endpoint homotopies. Adjoining the missing comparison and the upper completion gives a retractable upper cellular weak equivalence. The tree argument thus supplies the required joint lift.

🏷️ The final retract argument

Let $i:X\to Y$ be the elementary expansion and $r:Y\to X$ its unit retraction. Cellularity of $X$ and the lifting property of $p_0$ give $h:X\to \mathcal{P}X$ with $p_{0}h=\mathrm{id}$. Put

$$u=p_{1}h,\bar{u}=ur.$$

Both endpoints are weak equivalences, so $u$ is a weak equivalence. Naturality gives a commuting square with top map $\mathcal{P}(i)h$ and bottom pair $({\mathrm{id}}_Y,i\bar{u})$. The joint endpoint map lifts $J_n$, hence its actual pushout $i$, producing $f:Y\to \mathcal{P}Y$ with

$$p_{0}f={\mathrm{id}}_Y,p_{1}f=iur.$$

Therefore $v=iur$ is a weak equivalence. The arrow $iu:X\to Y$ is a retract of $v:Y\to Y$: use $i,r$ on domains and the identity on codomains. The identities $vi=iu$, $(iu)r=v$ and $ri=\mathrm{id}$ verify the retract. Hence $iu$ is a weak equivalence, and cancellation with $u$ proves that $i$ is one too.

All maps are morphisms of full models. The attaching cell can therefore be an arbitrary composite or coherence cell; it need not be a generator of a chosen cellular presentation.

To remove the cutoff for a test in dimension $k$, choose

$$q\ge \max \{n+1,k+1\}.$$

The reflector preserves the pushout and every cell involved, including the $(k+1)$-dimensional homotopy witness. Both the source disk and its witness obtained after reflection are thus actual cells before reflection. Choosing only $q=k$ would lose precisely the witness needed for this conclusion.

🏷️ Consequences and formalization scope

A model is cofibrant when it is a retract of a boundary-cellular model. The expansion theorem extends to these retracts. Together with the small-object argument, it gives the claimed canonical left semi-model structure. Cofibration–trivial-fibration factorization and lifting hold for all maps; trivial-cofibration–fibration factorization and lifting are required for cofibrant domains. Every object is fibrant. This is the stated semi-model conclusion, with its domain restriction retained.

Henry’s comparison theorem then applies to the category of finite cellular models and its completion. The manuscript obtains a realization–fundamental-infinity-groupoid Quillen equivalence with spaces, and therefore an equivalence after inverting weak equivalences. The resulting homotopy theory is independent of the chosen coherator within the convention specified above.

The repository’s family scope page documents the elementary-expansion weak-equivalence theorem for boundary-cellular models. It explicitly excludes the later semi-model structure and full comparison with spaces. No Lean build or equivalence audit is performed in this post.

The selected source review checks the convention, cutoff, induction dependencies, tree promotion, skeletal gluing, natural operation interpretation, endpoint lifting and final retract argument. The complete fixed-boundary homotopy calculus and the external recognition/comparison results remain source inputs rather than independently verified foundations here.

🏷️ Key steps and proof outlines

A one-dimensional expansion illustrates the coherence problem

Take $n=1$ and an arrow $a:x\to y$ in $X$. The expansion introduces a second arrow $a^{\prime }:x\to y$ and a two-cell $\alpha :a\Rightarrow a^{\prime }$. If $b:y\to z$ is another arrow, the free model also contains composites using $a^{\prime }$, and higher operations relating those composites to ones using $a$. Contracting the visible pair $(a^{\prime },\alpha )$ on generators therefore does not by itself establish a statement about the entire free model.

The partial cylinder is stationary on vertices in this example. Its one-dimensional component records a two-cell between arrows with fixed endpoints. Its next component must record a homotopy between two-cells while retaining both endpoint two-cells and the already chosen boundary cylinders. Those are the two-sided prescribed data $A_2^{01}$. A one-sided object $A_2^0$, by contrast, retains only one endpoint two-cell and is used to solve an endpoint lifting problem.

This example explains why both prescribed-data objects are needed. Keeping only one endpoint when defining operations would not force the other endpoint map to preserve those operations. Prescribing both endpoints everywhere would not give the one-sided retractions used to prove endpoint lifting. The construction solves these two tasks separately. (OpenAI, 2026)

Exact boundaries turn surjectivity into injectivity one dimension higher

Suppose a model map satisfies the exact-boundary test. Given two parallel source arrows $u,v$ and a target two-cell $f(u)\Rightarrow f(v)$, apply that test in dimension two with boundary exactly $(u,v)$. It produces a source two-cell $u\Rightarrow v$. Thus the map reflects homotopy of arrows. The same argument in dimension $r+1$ reflects homotopy of parallel $r$-cells; dimension one reflects connectedness of vertices.

The word “exactly” matters. A source cell whose boundary is only homotopic to $(u,v)$ would first require compatible changes of boundary, and those corrections must themselves be controlled. The manuscript proves the needed division and boundary-change lemmas before establishing the equivalence of this test with the homotopy-group definition.

The test also explains filtered-colimit closure without injective transition maps. A disk, its finite boundary, and the equations identifying its faces all occur together at some sufficiently late stage. Apply the test there and send the disk and its joining homotopy to the colimit. One must move far enough to realize the equations as well as their underlying cells; choosing a stage containing representatives alone is insufficient.

Shared faces are glued once, by a universal property

For a finite globular shape $S$, begin with its free model and adjoin cylinders skeleton by skeleton. At dimension $\ell$, a map from the new stage to a target consists of the old-stage map and, for each actual $\ell$-cell, a map from $P_{\ell }$ agreeing on its prescribed one-sided data. That agreement is precisely a map from $A_{\ell }^{ϵ}$.

Hence the new stage is the pushout attaching one copy of $P_{\ell }$ along $A_{\ell }^{ϵ}$ for each cell. If two cells share a face, both use the same map already fixed on the preceding skeleton. This is why the argument applies to real pasting schemes without accidentally duplicating an interface or adding incompatible independent choices.

Contractibility of the initial whiskered shape and the previously established upper-attachment result propagate through this filtration. Operations are then chosen as maps between the representing cylinder objects, once for each coherator generator. Precomposition evaluates them in every target, so naturality follows automatically; choosing unrelated fillers separately in each target would not have this property.

The cutoff must retain the witness, not just the question

A test of dimension $k$ asks for a $k$-cell and a $(k+1)$-cell witnessing its comparison with the target. Therefore the final cutoff must satisfy

$$q\ge \max \{n+1,k+1\}.$$

The term $n+1$ retains the expansion itself; $k+1$ retains the homotopy witness. After proving the theorem in the reflected category, every cell in that witness is unchanged by reflection, so it is an actual witness in the original model. Retaining only cells through $k$ would leave the conclusion potentially supplied by an artificial unique higher filler. This dimension check is what makes the finite-cutoff argument prove the unrestricted elementary-expansion theorem.

🏷️ Manuscripts and verification scope

• The Grothendieck homotopy hypothesis via elementary expansions — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. The documented formalization covers the elementary-expansion weak-equivalence theorem for every coherator in the Ara–Henry convention and every boundary-cellular model. It explicitly excludes the later semi-model structure and full comparison with spaces. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. The Grothendieck homotopy hypothesis via elementary expansions.