Prove ThomasonModelStructures (openai/math family 317: Thomason model structures in every strict higher…
Prove ThomasonModelStructures (openai/math family 317: Thomason model structures in every strict higher…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 317 of the release, Thomason model structures in every strict higher dimension…
The task
Context: this statement belongs to family 317 of the release, *Thomason model structures in every strict higher dimension* (Topology). The family as a whole: Resolves the Ara–Maltsiniotis conjecture: for every $n\ge1$ and $n=\omega$, small strict globular $n$-categories admit proper combinatorial Thomason model…
Part of raising-heart/openai-math.