# Thomason model structures in all strict higher dimensions

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Thomason Model Structures in Every Strict Higher Dimension](../../preprints/Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026/paper.pdf)

## Scope

The formalization proves the higher-dimensional Thomason model-structure theorem for small strict globular $n$-categories in every positive finite dimension and in dimension $\omega$. Each category has the stated proper combinatorial model structure, Quillen equivalent to simplicial sets through the twice-subdivided categorification and twice-extended Street nerve adjunction.

The selected statements also identify weak equivalences by the Street nerve in all these dimensions. Thus the constructions model the homotopy theory of spaces throughout the stated range.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Thomason model structures and nerve detection in all positive strict dimensions | [ThomasonModelStructures.lean](../ComparatorChallenges/ThomasonModelStructures.lean) |