Naturality for higher-dimensional path types

Chiara Sarti; Ioannis Markakis; Jamie Vicary; Thibaut Benjamin; Wilfred Offord

REVIEW 3 major objections 5 minor 45 references

Naturality for higher-dimensional path types

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A well-founded recursion builds naturality witnesses for operations of weak omega-categories, from which cylinder composites, stacking, and cone composites follow in all dimensions, machine-checked by a proof assistant.

desk verdict A genuinely new depth-1 naturality meta-operation for weak omega-categories, with real payoff for cylinder and cone composites; the proof has two fixable gaps that should be addressed before publication. read the letter →

arxiv 2501.11620 v3 pith:U4TOS5AU submitted 2025-01-20 math.CT cs.LO

Thibaut Benjamin , Ioannis Markakis , Wilfred Offord , Chiara Sarti , Jamie Vicary This is my paper · ORCID

classification math.CTcs.LO

keywords dependenttypetheoryidentitytypeshighercategoriesnaturalityweakomega-categoriescylindercompositesconeparametricity

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper tries to establish that weak $\omega$-category operations admit a systematic naturality construction: a meta-operation in the dependent type theory Catt (whose models are weak globular $\omega$-categories) that, from any term $t$ and any up-closed set $X$ of variables of depth at most 1, builds a well-typed naturality term $t \uparrow X$ in a duplicated context $\Gamma \uparrow X$, with a proof (Theorem 3.1) that the mutually recursive construction terminates and is correct. Geometrically the construction is a local tensor product with a directed interval; logically it is a globular analogue of Reynolds parametricity. The payoff is a power tool for term generation: the same mechanism produces cylinder composites and cylinder stacking (Section 4) and cone composites (Section 5) for weak $\omega$-categories, previously known only in the strict case or in low dimensions, and it exports the resulting terms to homotopy type theory as explicit inhabitants of higher path types. A reader should care because explicit cylinder and path-object constructions are the missing computational ingredient for model structures on weak $\omega$-categories.

What carries the argument

The carrying object is the naturality construction itself: a mutual recursion on the derivation trees of Catt that, for depths $d \in \{-1,0,1\}$ and $k \in \{0,1\}$, builds six families of outputs — duplicated contexts $\Gamma \uparrow X$ with two injections $\mathrm{in}^{\pm}$, type naturality $A \uparrow^t X$, term naturality $t \uparrow X$, substitution naturality $\sigma \uparrow X$, and naturality of coherence constructors $\mathrm{coh} \uparrow X$. The operative move is context duplication: each variable $x$ in the up-closed set $X$ gains a lower copy $x^-$, an upper copy $x^+$, and a filler cell $x^{\to}$ between them, which is exactly a local tensor product with the directed interval. Term naturality is assembled by cases: depth-0 terms use functoriality (the duplicated context is again a pasting context and the promoted type stays full, keeping the side condition that makes coherences well-typed), depth-1 linear composites are stacked from associators and whiskerings, reduced composites put a functorial core between two interchanger coherences, and general composites pass through the reduction of pasting contexts, with boundary-adjusting coherences on either side. The recursion is well-founded because derivations in Catt are unique, making induction on the derivation tree legitimate.

What would settle it

Run the companion proof assistant over small pasting contexts, generate $t \uparrow X$ for every up-closed set $X$ of depth at most 1, and type-check: the construction is correct only if every generated term is well-typed and the recursion terminates. The sharpest test is the general-composite case of Section 3.2(6)(iii), which passes through the reduction substitution; a pasting context whose reduced version fails to have the same source and target, or for which the $\alpha$-equivalence of Lemma B.21 fails, would refute Theorem 3.1.

Watch

Extended reading notes

Core claim

The central claim, Theorem 3.1, is that the recursive construction of naturality is well-founded and that its outputs satisfy judgements (1)-(6). Given a context $\Gamma$ and an up-closed set $X$ of its variables (if a variable in $X$ appears in the source or target of another variable, that other variable is also in $X$) with depth at most 1, and a term $t$ whose $X$-variables also have depth at most 1, the construction produces a term $t \uparrow X$ valid in the duplicated context $\Gamma \uparrow X$, where each variable $x \in X$ is split into a lower copy $x^-$, an upper copy $x^+$, and a filler cell $x^{\to}$ of type $x^- \to x^+$; it simultaneously produces types, substitutions, and naturality of coherence constructors. The depth-0 case is functoriality and was already known; the depth-1 case is genuine naturality, and it is exactly this case that yields the cylinder composites, cylinder stacking, and cone composites of Sections 4 and 5. Because the construction is a meta-operation on the syntax of Catt, the generated terms can be checked by machine and exported to homotopy type theory.

Load-bearing premise

The load-bearing premise is that every pasting context has a reduced pasting context with the same source and target, reached by a reduction substitution; this is a theorem taken, without proof, from a companion preprint by two of the present authors, and the general-composite case of the naturality construction, hence the cone and cylinder composites, collapses if that theorem fails.

Editorial extensions

If this is right

For any dimensions $m,n$ and direction $k$, two cylinders meeting along their $k$-boundary admit a composite $m \ast^{\square}_{k} n$, and two cylinders with matching bottom admit a vertical stacking $a \boxminus b$ (Theorems 4.2 and 4.3); these were previously known in full generality only in the strict case.
Cone composites $m \ast^{\triangle}_{k} n$ exist in all dimensions (Theorem 5.2); the paper states this is the first construction of cone composites in the weak $\omega$-category setting.
Every generated term can be exported to homotopy type theory, giving explicit computation of inhabitants of higher-dimensional path types (identity types), a concrete interface between coherence machinery and HoTT.
The cylinder construction is a step toward the long-sought path-object construction for weak $\omega$-categories, the missing component for a model structure on weak $\omega$-categories, and toward a weak $\omega$-category of weak $\omega$-categories.
All generated terms are type-checked in the implementation; artifact sizes grow rapidly (818, 10,236, 67,498, 509,702 bytes for the horizontal cylinder composites in dimensions 2 through 5), so computer memory currently bounds what can be computed on a workstation.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The depth restriction (variables in $X$ of depth at most 1) is presumably the main boundary of the method, not a deep one: the paper itself notes that higher-depth cases would govern weak higher transfors, so extending the recursion to greater depth is the natural next step.
Because the cylinder and cone composites are themselves produced by reapplying the naturality construction, the method suggests a general principle: any natural (depth-1) operation can be iterated into composite-forming operations in higher dimensions, potentially automating coherence generation beyond the geometric cases treated here.
Testable extension: the rapid growth of proof artifacts hints that sharing subterms (let-bindings or a DAG representation) could push feasible computations from dimension 5 to higher dimensions; this can be checked directly with the provided implementation.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The first thing you should know: this paper is a real advance, not a repackaging. The depth-1 naturality construction for Catt is new; the depth-0 functoriality was known, but lifting it to variables of depth 1 and using it to produce explicit cylinder composites for n>=4 and cone composites in the weak setting is original. The authors are careful about what is new: they credit the n=3 cylinder composites to Henry-Lanari and claim only n>=4 for cylinders, and the first cone composites in the weak setting. That restraint is credible.

The paper also does a lot of hard work. The mutual recursion over contexts, types, terms, substitutions, and term constructors is laid out in detail, and the proof of Theorem 3.1 is a genuine inductive argument, not a hand-wave. The implementation is a real check: the generated terms are huge, and type-checking them gives non-trivial evidence that the construction is coherent. I found the examples in the introduction genuinely useful for getting a feel for what the construction does.

Now the soft spots, in proportion. First, the inductive step for linear composites (Lemma B.17) uses a suspension commutation that Lemma B.16 does not actually provide as stated. Lemma B.16 only proves suspension commutes with depth-0 naturality (and for types at depth 1), but the linear composite case needs it for depth-1 terms. The proof says the result is 'immediate' and cites Lemma B.16; on reading, it is not immediate. This looks fixable, but it is a genuine gap in the written proof.

Second, the general composite case in Section 3.2(6)(iii) leans entirely on a reduction theorem from [13], a preprint by two of the present authors. The reduction substitution rho_Gamma is what lets the construction reduce any pasting context to a reduced one. If that theorem is wrong, the naturality of arbitrary composite coherences, and hence the cylinder and cone composites of Sections 4-5, is not well-defined. This is a heavy load-bearing citation, and the paper does not re-prove it. It is not circular, and I have no reason to think [13] is false, but the dependence should be explicit and the result should be verifiable.

Minor: the code is described but no URL or hash is given, which makes the supplementary material hard to inspect.

Overall: the central construction is plausible, the depth-0 and reduced cases are proved, and the machine-checked examples support the claims. The two gaps are real but likely repairable. This paper deserves a serious referee. I would send it to peer review and ask the authors to fix the suspension commutation and to either prove or clearly isolate the reduction-theorem dependency.

Referee Report

3 major / 5 minor

Summary. The paper defines a meta-operation in the dependent type theory Catt that, for any up-closed set X of variables of depth at most 1 in a context, produces a naturality cell t↑X for any term t, together with analogous constructions for contexts, types, substitutions and coherence constructors. The main result is Theorem 3.1, which asserts that the recursive construction is well-founded and that all generated terms satisfy the stated typing judgements. The paper then applies this construction to define horizontal composites and stacking of cylinders (Section 4) and composites of cones (Section 5), and reports a proof-assistant implementation that type-checks all examples (Section 6). The technical development is largely self-contained, but a central case of the main theorem, the naturality of general composites in Section 3.2(6)(iii), depends on a reduction theorem for pasting contexts cited from the same-author preprint [13], and Lemma B.21 additionally uses a strict-ω-category composition fact for Batanin trees without proof.

Significance. If the main theorem is correct, the paper makes a substantial contribution: it provides a uniform, type-theoretic construction of naturality for all operations of weak ω-categories, with a geometric interpretation as a local tensor product with the directed interval. The resulting explicit cylinder composites and cone composites are new in the weak setting for dimensions ≥ 4 and ≥ 2 respectively, and the implementation provides machine-checked witnesses for the stated types, which is a genuine strength. The dependence of the central theorem on an external reduction theorem is currently the main obstacle to accepting the paper as fully self-contained.

major comments (3)

[Section 3.2(6)(iii) and proof of Theorem 3.1] The general composite case of the naturality construction is defined using the assertion, cited from [13, Section 4.4], that every pasting context Γ has a reduced pasting context Γ_r with the same source and target and a reduction substitution ρ_Γ. This assertion is load-bearing: without it, coh_{Γ,A}↑X is undefined for every non-reduced depth-1 composite, so Theorem 3.1 fails for that branch. Since [13] is a preprint by two of the present authors and the needed statement is not proved or even stated precisely in this paper, please either include a proof of the reduction theorem in an appendix, or state it explicitly as an assumption and mark which parts of Theorem 3.1 are conditional on it.
[Appendix B, Lemma B.21] The proof of Lemma B.21 asserts that ∂^-Ψ ≅ ∂^-Γ because composition of Batanin trees satisfies the rules of strict ω-categories, citing [8]. This is a nontrivial strictification claim, and it is used to justify the interchangers j^± in the reduced-composite construction, which are in turn needed for Theorem 3.1(6). The paper does not provide the required derivation or a precise reference with a statement matching this use. Please expand this step or supply a reference that proves the exact identification used.
[Section 3.2(6)(i) and Lemma B.17] The inductive step for linear composites claims that suspension commutes with the depth-1 naturality for the contexts Ψ^n_k, using Lemma B.16. However, Lemma B.16 is stated for X of depth 0 in the unsuspended context Γ, while X has depth 1 in Ψ^n_k. The intended reading is presumably that depth-1 variables of Ψ^n_k are suspensions of depth-0 variables of Ψ^{n-1}_k, but this is not stated. As written, the proof of Lemma B.17 does not justify the application of Lemma B.16. Please make this correspondence explicit.

minor comments (5)

[Section 1] The reference to 'Bernady et al.' should be 'Bernardy et al.'.
[Section 2.3] There is a typo in the sentence 'We present a brief overview of those that we use use in this article'; delete the second 'use'.
[Section 6] The command 'cylcone(3,1,3)' appears to be a typo for 'cylcomp(3,1,3)'; please correct it for consistency with the other built-ins.
[Appendix B, Lemma B.19] The notation in∓ is used without definition; please define it or avoid the ∓ symbol, since the reader otherwise has to infer it as the dual of in±.
[Appendix D] In the description of the interchangers, the phrase 'Deﬁnes to be the source of of the type' contains a duplicated word and should be rephrased.

Circularity Check

1 steps flagged · score 4.0 of 10

General composite naturality is defined via a reduction substitution imported from a same-author preprint ([13, Sec. 4.4]); Lemma B.21 uses the same black box, making that branch of Theorem 3.1 load-bearing self-citation.

self citation load bearing [Section 3.2(6)(iii), "Naturality of General Composites"; also Lemma B.21 and proof of Theorem 3.1, case d=1, general composites.]
"For the general case, we will use that every pasting context Γ gives rise to a reduced pasting context Γ r with the same source and target, along with a reduction substitution Γ ⊢ ρΓ : Γ r. This substitution acts as the identity on the boundary, and sends maximal-dimensional variables of Γ r to linear composites of maximal-dimensional variables of Γ [13, Section 4.4]."

Clause (6)(iii) defines the naturality of a general composite coherence only after importing the existence and exact boundary/linear-composite properties of ρΓ from [13, Section 4.4], a preprint by two of the present authors. The definition is literally built on that substitution: c′Γ,X,A = (coh Γr,A ↑ ρ−1Γ(X))[ρΓ ↑ X], and the proof of Theorem 3.1 delegates exactly this case to the cited reduction theorem. Lemma B.21 uses the same theorem, together with asserted facts about Batanin-tree composition, to identify Ψr with Γ. No proof of the reduction theorem is included or independently checked in the present paper.

full rationale

The construction is largely self-contained and genuinely inductive: the paper defines naturality for variables, substitutions and linear/reduced composites, and proves the relevant typing judgements for those cases; the proof assistant also checks the generated examples. The main concern is local and citation-borne. In Section 3.2(6)(iii), the general-composite case is defined through the reduction substitution ρΓ whose existence and boundary/linear-composite properties are imported from [13, Section 4.4], a preprint by two of the present authors, and Lemma B.21 uses that same theorem as a black box. This is not a fitted parameter renamed as a prediction, nor is the target typing judgement assumed in its own definition. It is, however, a load-bearing same-author citation: if the reduction theorem failed, cohΓ,A↑X would be undefined for every non-reduced depth-1 composite, including the smallest pasting contexts needed for associator-like coherences. The paper also relies on the first author's thesis [10] for structural facts such as [10, Lemma 87] that Γ↑X is a pasting context, though the main depth-1 cases are argued locally. Because the central claim retains substantial independent content and the dependency is an imported theorem rather than a definitional equivalence, the score is 4 rather than higher.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

No numeric parameters are fitted and no new entities are postulated. The construction is defined inside Catt and its correctness depends on standard meta-properties of that type theory and on prior results about pasting contexts and suspension, several of which come from the same research group.

assumptions (6)

domain assumption Catt derivations are unique (Finster-Mimram, [24, Lemma 7]).
Used to justify mutual recursion on derivation trees in Section 3.1.
domain assumption Every pasting context admits a reduction to a reduced pasting context with the same source and target ([13, Section 4.4]).
Used in Section 3.2(6)(iii) for general composites; result from same authors' preprint, not re-proved.
domain assumption Depth-0 naturality preserves pasting contexts and fullness ([10, Lemmas 87-90]).
Cited for the depth-0 case and used in Lemma B.10; the paper re-proves the main depth-0 typing cases.
domain assumption Suspension and opposite meta-operations are correct ([10], [12]).
Used for linear composites, cylinders and cones in Sections 3.2(6)(i), 4 and 5.
standard math Composition of Batanin trees satisfies the rules of strict omega-categories ([8]).
Used in Lemma B.21 and in defining interchangers via composition of pasting contexts.
standard math Pasting contexts have no non-trivial isomorphisms ([17, Lemma 1.7]).
Used in Lemma B.21 to upgrade an isomorphism between pasting contexts to alpha-equivalence.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Naturality for higher-dimensional path types." pith.science (2026). https://pith.science/paper/U4TOS5AU

@misc{pith2026250111620,
  author       = {Pith},
  title        = {Pith review of: Naturality for higher-dimensional path types},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/U4TOS5AU}},
  note         = {Machine review of arXiv:2501.11620}
}

read the original abstract

We define a naturality construction for the operations of weak omega-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a ``power tool'' to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in omega-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants.

Figures

Figures reproduced from arXiv: 2501.11620 by the authors.

**Figure 1.** Depths of variables in a context. can be understood as a functoriality construction, which has already been described [10]. The higher-depth cases, which are beyond our present work, would likely govern the behaviour of weak higher transfors [21]. We have implemented our naturality construction as a meta-operation in an existing proof assistant for Catt, and all of our examples have been demonstrated in the implem… view at source ↗

**Figure 2.** Grammar for the raw syntax of Catt. Acknowledgements We would like to express our gratitude to Eric Finster for many insightful discussions. We also thank Dimitri Ara, Fran¸cois M´etayer and Alex Rice for helpful comments. 2 Globular Higher Categories 2.1 Introducing the Type Theory We give a complete but concise presentation of the dependent type theory Catt introduced by Finster and Mimram [24] to model weak ω-ca… view at source ↗

**Figure 3.** Derivation rules for Catt For contexts, substitutions, and terms consisting of variables, the rules for those judgements are the standard ones of dependent type theory (see [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

Figures from the paper (18 more)

**Figure 4.** Figure 4: Derivation rules for pasting contexts 9 [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]

**Figure 5.** Figure 5: A pasting context and its boundaries displayed as t [PITH_FULL_IMAGE:figures/full_fig_p011_5.png]

**Figure 6.** Figure 6: Suspension and opposite of a context. where Γ′ is the unique pasting context isomorphic to opM Γ, up to α-equivalence, and opM Γ ⊢ opΓ M : Γ′ is the isomorphism. Benjamin and Markakis have established correctness of those meta-operations [10, 12], meaning that the fol…

**Figure 7.** Figure 7: Linear pasting contexts. of (n+1)-cells along their n-boundary, illustrated in [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]

**Figure 8.** Figure 8: The contexts Γ ↑ Xlm and Γ ↑ X. the remaining variables. The term cohΓ,A ↑ X is then given as follows: (a − ∗0h)∗1 ( g →∗0h) j − Γ,X,A −−−−→ ((a − ∗1 g →)∗0h −)∗1 (g + ∗0 h → ) cΓ,X,A −−−−→ (f − ∗0h → )∗1 ((f → ∗1 a +)∗0h +) j + Γ,X,A −−−−→ (f → ∗0h)∗1 (a + ∗0h) (6)(ii…

**Figure 9.** Figure 9: The reduction of a pasting context. Lemma 3.2. Let Γ ⊢ and X ∈ Up(Γ) of depth at most 1. Then for a term Γ ⊢ t : A (resp. type Γ ⊢ A, substitution Γ ⊢ σ : ∆) whose variables do not intersect with X: t[in± Γ,X] = t σ ◦ in± Γ,X = σ A[in± Γ,X] = A Lemma 3.3. Let Γ ⊢ σ : ∆…

**Figure 10.** Figure 10: illustrates the contexts 2 and 3 . 2 : ⊤ − 1 ⊤ + 1 ⊥ − 1 ⊥ + 1 fill− 1 ⊤2 fill+ 1 fill2 ⊥2 3 : ⊤ − 1 ⊤ + 1 ⊥ − 1 ⊥ + 1 fill− 1 ⇓ fill+ ⇚ 1 ⇓ [PITH_FULL_IMAGE:figures/full_fig_p022_10.png]

**Figure 11.** Figure 11: Formula for the cylinder type for n ≥ 1. By construction, there exists a type ∂ n ⊢ Cyln such that n ⊢ filln : Cyln . An n-dimensional cylinder in a context Γ is a term Γ ⊢ t : Cyln [γ] for some substitution Γ ⊢ γ : ∂ n. Equivalently, it is a substitution Γ ⊢ hγ, fill…

**Figure 12.** Figure 12: Composites and stacking of 3-cylinders. Theorem 4.3. Given n-cylinders a, b in a context Γ such that (a) = (b), there exists an n-cylinder a ⊟ b, called the stacking and illustrated in [PITH_FULL_IMAGE:figures/full_fig_p025_12.png]

**Figure 13.** Figure 13: The first cone contexts. Conen+1(a, b, c) =    b → ( n−1 (b) ∗n−2 ((. . . ∗3 ( 2 (b)∗1 (a ∗0 1 (c))) ∗2 . . .) ∗n−3 n−2 (c))) ∗n−1 c if n is odd b ∗n−1 (( n−2 (b) ∗n−3 (. . . ∗3 ( 2 (b)∗1 (a ∗0 1 (c))) ∗2 . . .)) ∗n−2 n−1 (c)) → c if n is even [PITH_FULL_IMA…

**Figure 14.** Figure 14: Formula for the cone type for n ≥ 1. some substitution Γ ⊢ γ : ∂ n . Equivalently, it is a substitution Γ ⊢ hγ, filln 7→ ti : n. A substitution Γ ⊢ γ : ∂ n for n ≥ 2 is completely determined by the image of the variables basen, fill− n−1 and fill+ n−1 . Denoting those…

**Figure 15.** Figure 15: The two composites of 3-cones • A readme file with full details on building the proof assistant. This works on both Linux and Mac, and on Windows in the WSL subsystem. • Catt files encoding the examples from the introduction. • Artifacts storing a range of pre-compute…

**Figure 16.** Figure 16: The substitution ψ {x0,x1,f0,f1} 2,1 . Definition A.4. Let 0 ≤ j < k and X ∈ Up(Ψ0 k ) such that fj ∈ X. We define the whiskering phase w X k,j to be the unbiased composition w X k,0 = f0 → ∗0 f1[in+ Ψ0 k ,X] ∗0 · · · ∗0 fk−1[in+ Ψ0 k ,X] w X k,j = f0[in− Ψ0 k ,X] ∗0 …

**Figure 17.** Figure 17: The construction of Φ and Ψ in j − Γ,X,A. the type theory Catt, as depicted in [PITH_FULL_IMAGE:figures/full_fig_p036_17.png]

**Figure 17.** Figure 17: It follows that the two terms are composable, so [PITH_FULL_IMAGE:figures/full_fig_p050_17.png]

**Figure 18.** Figure 18: The cylinder contexts of dimension 2 and 3 of [PITH_FULL_IMAGE:figures/full_fig_p054_18.png]

**Figure 11.** Figure 11: Given two cylinders Γ ⊢ m : Cylk+1(a0, b0, c, d) Γ ⊢ n : Cylk+1(a1, b1, d, e) we consider the following term: u = Σ( k ∗ k k−1 )(m, n) By induction, this term satisfies the following judgement, which is not exactly the desired type: Γ ⊢ u : Cylk+1   (a0 ∗0 1 (c)) ∗k…

**Figure 19.** Figure 19: The Cone contexts of dimension 2 and 3 of [PITH_FULL_IMAGE:figures/full_fig_p057_19.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

45 extracted references · 30 canonical work pages

[13]

‘Invertible cells in ω-categories’

Thibaut Benjamin and Ioannis Markakis. ‘Invertible cells in ω-categories’

work page
[8]

Michael A. Batanin. ‘Monoidal Globular Categories As a Natural En viron- ment for the Theory of Weak n-Categories’. In: Advances in Mathematics 136.1 (1998), pp. 39–103. doi: 10.1006/aima.1998.1724

arXiv 1998
[1]

‘A Syntactical Appro ach to Weak ω-Groupoids’

Thorsten Altenkirch and Ondrej Rypacek. ‘A Syntactical Appro ach to Weak ω-Groupoids’. In: 21st Annual Conference of the EACSL (CSL 2012). 2012. doi: 10.4230/LIPICS.CSL.2012.16

work page doi:10.4230/lipics.csl.2012.16 2012
[2]

‘Sur les ∞-groupo ¨ ıdes de Grothendieck et une variante∞- cat´ egorique’

Dimitri Ara. ‘Sur les ∞-groupo ¨ ıdes de Grothendieck et une variante∞- cat´ egorique’. Th` ese de doctorat. Universit´ e Paris Diderot (Paris 7), 2010

work page 2010
[3]

‘The folk model category structur e on strictω-categories is monoidal’

Dimitri Ara and Maxime Lucas. ‘The folk model category structur e on strictω-categories is monoidal’. In: Theory and Applications of Categories 35 (2020), pp. 745–808. arXiv: 1909.13564

arXiv 2020
[4]

‘Joint et tranches pour les ∞- cat´ egories strictes’

Dimitri Ara and Georges Maltsiniotis. ‘Joint et tranches pour les ∞- cat´ egories strictes’. In:M´ emoires de la Soci´ et´ e math´ ematique de France 165 (2020), pp. 1–213. doi: 10.24033/msmf.473

work page doi:10.24033/msmf.473 2020
[5]

Baez and James Dolan

John C. Baez and James Dolan. ‘Higher-dimensional algebra and to po- logical quantum ﬁeld theory’. In: Journal of Mathematical Physics 36.11 (1995), pp. 6073–6105. doi: 10.1063/1.531236. 29

doi:10.1063/1.531236 1995
[6]

‘Modular categories as representations of the 3- dimensional bordism 2-category’

Bruce Bartlett et al. ‘Modular categories as representations of the 3- dimensional bordism 2-category’. 2015. arXiv: 1509.06811

arXiv 2015

Show all 45 references

[7]

Michael A. Batanin. Computads and slices of operads. 2002. arXiv: math/0209035. url: http://arxiv.org/abs/math/0209035 (visited on 18/02/2023). Pre- published

2002 arXiv
[9]

‘Introduction to bicategories’

Jean B´ enabou. ‘Introduction to bicategories’. In: Reports of the Midwest Category Seminar. Vol. 47. Lecture Notes in Mathematics. 1967, pp. 1–77. doi: 10.1007/BFb0074299

1967 doi
[10]

‘A type theoretic approach to weak ω-categories and related higher structures’

Thibaut Benjamin. ‘A type theoretic approach to weak ω-categories and related higher structures’. Th` ese de doctorat. Institut Polyte chnique de Paris, 2020

2020
[11]

‘Generating Higher Identity Proofs in Homoto py Type Theory’

Thibaut Benjamin. ‘Generating Higher Identity Proofs in Homoto py Type Theory’. 2024. arXiv: 2412.01667

2024 arXiv
[12]

Hom ω-Categories of a Com- putad Are Free

Thibaut Benjamin and Ioannis Markakis. Hom ω-Categories of a Com- putad Are Free. 2024. arXiv: 2402.01611

2024 arXiv
[14]

‘CaTT cont exts are ﬁnite computads’

Thibaut Benjamin, Ioannis Markakis and Chiara Sarti. ‘CaTT cont exts are ﬁnite computads’. In: Electronic Notes in Theoretical Informatics and Computer Science. Vol. 4 - Proceedings of MFPS XL. 2024, 5. doi: 10.46298/entics.14675

2024 doi
[15]

‘Globular Weak ω- Categories as Models of a Type Theory’

Thibaut Benjamin, Samuel Mimram and Eric Finster. ‘Globular Weak ω- Categories as Models of a Type Theory’. In: Higher Structures 8.2 (2024), pp. 1–69. doi: 10.21136/HS.2024.07

2024 doi
[16]

‘Types are weak ω-groupoids’

Benno van den Berg and Richard Garner. ‘Types are weak ω-groupoids’. In: Proceedings of the London Mathematical Society 102.2 (2011), pp. 370–

2011
[17]

‘A Cellular Nerve for Higher Categories’

Clemens Berger. ‘A Cellular Nerve for Higher Categories’. In: Advances in Mathematics 169.1 (2002), pp. 118–175. doi: 10.1006/aima.2001.2056

2002
[18]

‘P roofs for Free: Parametricity for Dependent Types’

Jean-Philippe Bernardy, Patrik Jansson and Ross Paterson. ‘P roofs for Free: Parametricity for Dependent Types’. In: Journal of Functional Pro- gramming 22.2 (2012), pp. 107–152. doi: 10.1017/S0956796812000056

2012 doi
[19]

‘Iterated algebraic injectivity and the faithfulne ss conjec- ture’

John Bourke. ‘Iterated algebraic injectivity and the faithfulne ss conjec- ture’. In:Higher Structures 4.2 (2020), pp. 183–210. doi: 10.21136/HS.2020.13

2020 doi
[20]

‘Orientals and Cubes, Indu ctively’

Mitchell Buckley and Richard Garner. ‘Orientals and Cubes, Indu ctively’. In: Advances in Mathematics 303 (2016), pp. 175–191. doi: 10.1016/j.aim.2016.07.026

2016 doi
[21]

Sjoerd E. Crans. ‘Localizations of Transfors’. In: K-Theory 28.1 (2003), pp. 39–105. doi: 10.1023/A:1024186923002. 30

2003 doi
[22]

‘Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Chur ch- Rosser theorem’

N.G De Bruijn. ‘Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Chur ch- Rosser theorem’. In:Indagationes Mathematicae (Proceedings)75.5 (1972), pp. 381–392. doi: 10.1016/1385-7258(72)90034-0

1972 doi
[23]

Dean et al

Christopher J. Dean et al. ‘Computads for weak ω-categories as an in- ductive type’. In: Advances in Mathematics 450 (2024), p. 109739. doi: 10.1016/j.aim.2024.109739

2024
[24]

‘A type-theoretical deﬁnition o f weak ω-categories’

Eric Finster and Samuel Mimram. ‘A type-theoretical deﬁnition o f weak ω-categories’. In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) . ACM, 2017, pp. 1–12. doi: 10.5555/3329995.3330059

2017
[25]

‘Algebraic models of homotopy types and the homot opy hypothesis’

Simon Henry. ‘Algebraic models of homotopy types and the homot opy hypothesis’. 2016. arXiv: 1609.04622

2016 arXiv
[26]

‘On the homotopy hypothesis in di- mension 3’

Simon Henry and Edoardo Lanari. ‘On the homotopy hypothesis in di- mension 3’. In: Theory and Applications of Categories 39 (2023), pp. 735– 768

2023
[27]

‘A folk model structure on omega-cat’

Yves Lafont, Fran¸ cois M´ etayer and Krzysztof Worytkiewicz. ‘A folk model structure on omega-cat’. In:Advances in Mathematics 224.3 (2010), pp. 1183–

2010
[28]

‘A semi-model structure for Grothendieck we ak 3-groupoids’

Edoardo Lanari. ‘A semi-model structure for Grothendieck we ak 3-groupoids’
[29]

‘Towards a globular path object for weak ∞-groupoids’

Edoardo Lanari. ‘Towards a globular path object for weak ∞-groupoids’. In: Journal of Pure and Applied Algebra 224.2 (2020), pp. 630–702. doi: 10.1016/j.jpaa.2019.06.004

2020 doi
[30]

‘Weak ω-Categories from Intensional Type The- ory’

Peter LeFanu Lumsdaine. ‘Weak ω-Categories from Intensional Type The- ory’. In:Typed Lambda Calculi and Applications. Vol. 5608. 2009, pp. 172–

2009
[31]

‘Derived algebraic geometry’

Jacob Lurie. ‘Derived algebraic geometry’. PhD thesis. Massach usetts In- stitute of Technology, Dept. of Mathematics, 2004

2004
[32]

Higher Topos Theory

Jacob Lurie. Higher Topos Theory. Annals of Mathematics Studies n ◦ 170. Princeton, N.J: Princeton university press, 2009

2009
[33]

‘Grothendieck ∞-groupoids, and still another deﬁn- ition of ∞-categories’

Georges Maltsiniotis. ‘Grothendieck ∞-groupoids, and still another deﬁn- ition of ∞-categories’. 2010. arXiv: 1009.2331 [math]

2010 arXiv
[34]

‘Towards 3-Dimensional Rewriting Theory’

Samuel Mimram. ‘Towards 3-Dimensional Rewriting Theory’. In: Logical Methods in Computer Science 10.2 (2014), p. 1. doi: 10.2168/LMCS-10(2:1)2014

2014 doi
[35]

Reynolds

John C. Reynolds. ‘Types, Abstraction and Parametric Polymor phism’. In: Information Processing 83. Vol. 9. IFIP Congress Series. 1983, pp. 513– 523

1983
[36]

Schommer-Pries

Christopher J. Schommer-Pries. ‘The Classiﬁcation of Two-Dime nsional Extended Topological Field Theories’. PhD Thesis. Max Planck Institu te for Mathematics, Bonn, 2011. 31

2011
[37]

Robert A. G. Seely. ‘Modelling computations: a 2-categorical fr amework’. In: Logic in Computer Science . 1987

1987
[38]

‘The petit topos of globular sets’

Ross Street. ‘The petit topos of globular sets’. In: Journal of Pure and Ap- plied Algebra 154.1-3 (2000), pp. 299–315. doi: 10.1016/S0022-4049(99)00183-8

2000 doi
[39]

‘Generic morphisms, parametric representations and weakly cartesian monads.’ In: Theory and Applications of Categories 13 (2004), pp

Mark Weber. ‘Generic morphisms, parametric representations and weakly cartesian monads.’ In: Theory and Applications of Categories 13 (2004), pp. 191–234. 32 A Naturality of Coherences In this appendix, we provide the full deﬁnition of the naturality of line ar com- positions ...

2004
[43]

z =fj+1 ∈X and y =fj
[44]

z =xj+1 ∈X and y =fj ∈X
[45]

In the ﬁrst case, xj+1 /∈X, hence the phases are respectively of the form wX k,j+1 andwX k,j

z =fj ∈X and y =xj ∈X. In the ﬁrst case, xj+1 /∈X, hence the phases are respectively of the form wX k,j+1 andwX k,j . By Lemma B.13, the target of the former and the source of the lat ter both compute to: f0[in−] ∗0... ∗0f − j ∗0f + j+1 ∗0... ∗0f [in+] In the second case, the ...
[187]

doi: 10.1007/978-3-642-02273-9_14

doi
[394]

doi: 10.1112/plms/pdq026

doi
[1231]

doi: 10.1016/j.aim.2010.01.007

2010 doi

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [13]

‘Invertible cells in ω-categories’

Thibaut Benjamin and Ioannis Markakis. ‘Invertible cells in ω-categories’

work page

[2] [8]

Michael A. Batanin. ‘Monoidal Globular Categories As a Natural En viron- ment for the Theory of Weak n-Categories’. In: Advances in Mathematics 136.1 (1998), pp. 39–103. doi: 10.1006/aima.1998.1724

arXiv 1998

[3] [1]

‘A Syntactical Appro ach to Weak ω-Groupoids’

Thorsten Altenkirch and Ondrej Rypacek. ‘A Syntactical Appro ach to Weak ω-Groupoids’. In: 21st Annual Conference of the EACSL (CSL 2012). 2012. doi: 10.4230/LIPICS.CSL.2012.16

work page doi:10.4230/lipics.csl.2012.16 2012

[4] [2]

‘Sur les ∞-groupo ¨ ıdes de Grothendieck et une variante∞- cat´ egorique’

Dimitri Ara. ‘Sur les ∞-groupo ¨ ıdes de Grothendieck et une variante∞- cat´ egorique’. Th` ese de doctorat. Universit´ e Paris Diderot (Paris 7), 2010

work page 2010

[5] [3]

‘The folk model category structur e on strictω-categories is monoidal’

Dimitri Ara and Maxime Lucas. ‘The folk model category structur e on strictω-categories is monoidal’. In: Theory and Applications of Categories 35 (2020), pp. 745–808. arXiv: 1909.13564

arXiv 2020

[6] [4]

‘Joint et tranches pour les ∞- cat´ egories strictes’

Dimitri Ara and Georges Maltsiniotis. ‘Joint et tranches pour les ∞- cat´ egories strictes’. In:M´ emoires de la Soci´ et´ e math´ ematique de France 165 (2020), pp. 1–213. doi: 10.24033/msmf.473

work page doi:10.24033/msmf.473 2020

[7] [5]

Baez and James Dolan

John C. Baez and James Dolan. ‘Higher-dimensional algebra and to po- logical quantum ﬁeld theory’. In: Journal of Mathematical Physics 36.11 (1995), pp. 6073–6105. doi: 10.1063/1.531236. 29

doi:10.1063/1.531236 1995

[8] [6]

‘Modular categories as representations of the 3- dimensional bordism 2-category’

Bruce Bartlett et al. ‘Modular categories as representations of the 3- dimensional bordism 2-category’. 2015. arXiv: 1509.06811

arXiv 2015