{"id":"d92b8dbf-3dfb-466f-9db5-eb8b5b4dc850","arxiv_id":"2501.11620","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A depth-bounded naturality meta-operation in the Catt type theory constructs and machine-checks cylinder and cone composites in weak omega-categories.","lead":"The authors define a new naturality operation for weak higher categories and use it to build composition operations for cylinders and cones. The operation is implemented in a proof assistant, which checks that the generated terms have the correct type.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.1's general composite case is defined only through an unproved reduction theorem cited from a same-author preprint; if [13, Sec. 4.4] fails, naturality of arbitrary composite coherences is undefined.","rationale":"The reader's weakest_assumption pins down exactly the point on which Theorem 3.1 depends but does not prove. The construction of §3.2(6)(iii) is not an induction that can be filled in by the reader: its defining data e_{Γ,X,A}, c', and the final composite all presuppose the reduction substitution ρ_Γ. Unlike the depth-0 case, which is documented from [10], and the linear/reduced cases, which are proved in Appendices A and B, the general case is reduced to an external theorem. The paper is transparent about the citation, but that does not remove the dependency: [13] is a preprint by two of the same authors, and the required statement (existence of Γ_r and ρ_Γ with the stated properties) is not restated, let alone proved. Lemma B.21 is even more exposed: it needs Ψ^r = Γ up to α-equivalence and uses 'composition of Batanin trees satisfies the rules of strict ω-categories' and Berger's lemma on pasting contexts as additional black boxes. If any of these fail, the interchangers j^± in the reduced-composite clause fail, and the proof of Theorem 3.1 for depth-1 coherences collapses. I do not see a comparable gap elsewhere: the suspension issue raised by the reader is, on close reading, covered by the third clause of Lemma B.16 (Σ(A↑^tX) = (ΣA)↑^{Σt}X for depthX(t)=1), so it is not load-bearing. The implementation is real evidence for the computed examples, but the examples are mostly depth-0 or reduced cases; they do not certify the general-composite clause for arbitrary non-reduced pasting contexts. My recommendation is therefore to keep the reader's CONDITIONAL verdict, with the condition being an independent verification of the reduction theorem. If that verification succeeds, the theorem should be accepted; if it fails, the central claim is REJECT-worthy. Since my concern does not move the verdict, I choose UNCHANGED.","tokens_in":39599,"tokens_out":12997,"duration_ms":133662,"concrete_test":"Implement, independently of the paper's code, the reduction construction of [13, Section 4.4] for the non-reduced dimension-2 pasting context Γ = (x,y,z : ⋆; f,g : x→y; a : f→g; h : y→z), the context of Fig. 9. Verify in the Catt implementation that: (i) Γ_r has exactly the same source and target contexts as Γ; (ii) ρ_Γ is a well-typed substitution that is the identity on the boundary and maps maximal variables to linear composites; (iii) the coherence e_{Γ,X,A} of §3.2(6)(iii) type-checks for a full type A and an up-closed depth-1 X (e.g., X={f,g,a,h}). If any check fails, the general composite clause of Theorem 3.1 is unsupported; if all pass for this and for a battery of larger non-reduced contexts, the external dependency is validated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 3.2(6)(iii) defines naturality of a general composite coherence coh_{Γ,A}[id] by first invoking, without proof, the theorem 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 Γ ⊢ ρ_Γ : Γ_r that is the identity on the boundary and sends maximal-dimensional variables to linear composites of maximal-dimensional variables of Γ. The entire clause is built on this: e_{Γ,X,A} is a coherence between coh_{Γ,A}[id] and coh_{Γ_r,A}[ρ_Γ], c' is the reduced naturality transported along ρ_Γ ↑ X, and the final term is their composite. If ρ_Γ does not exist or lacks the stated properties, coh_{Γ,A}↑X is simply undefined for every non-reduced depth-1 composite, so Theorem 3.1 fails for that branch. This is not a cosmetic omission: Lemma B.21, needed to type the interchangers j^± in the reduced case, uses the same reduction theorem together with additional facts about Batanin-tree composition that are only asserted. The proof of Theorem 3.1 delegates exactly this case to [13], a preprint by two of the present authors, and gives no independent verification. The concern is concrete and local: one can isolate it by testing the smallest non-reduced pasting context with two 2-cells sharing a 1-boundary. If the reduction theorem fails there, the naturality of associator-like composites in dimension 2 is not well-founded.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":39874,"tokens_out":6405,"duration_ms":75436,"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":[{"comment":"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.","section":"Section 3.2(6)(iii) and proof of Theorem 3.1"},{"comment":"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":"Appendix B, Lemma B.21"},{"comment":"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.","section":"Section 3.2(6)(i) and Lemma B.17"}],"minor_comments":[{"comment":"The reference to 'Bernady et al.' should be 'Bernardy et al.'.","section":"Section 1"},{"comment":"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":"Section 2.3"},{"comment":"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.","section":"Section 6"},{"comment":"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±.","section":"Appendix B, Lemma B.19"},{"comment":"In the description of the interchangers, the phrase 'Defines to be the source of of the type' contains a duplicated word and should be rephrased.","section":"Appendix D"}],"recommendation":"major_revision","confidential_remarks":"The main risk is not circularity but the unproved dependence of the central theorem on the reduction theorem from [13], a preprint by two of the authors. If that theorem is accepted, the construction appears sound and the implementation is a strong check. I would ask for a self-contained statement and proof of the reduction theorem, or at least a precise reference to a peer-reviewed version, before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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.\n\nNow 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.\n\nSecond, 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.\n\nMinor: the code is described but no URL or hash is given, which makes the supplementary material hard to inspect.\n\nOverall: 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.","headline":"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.","tokens_in":40443,"tokens_out":7979,"would_cite":true,"duration_ms":81739,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["dependent type theory","identity types","higher categories","naturality","weak omega-categories","cylinder composites","cone composites","parametricity"],"falsifier":"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.","tokens_in":39374,"feed_emoji":"🔺","tokens_out":19137,"duration_ms":168385,"temperature":0.7,"pith_summary":"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.","feed_headline":"One recursion builds naturality for weak omega-category operations","feed_subtitle":"It builds explicit cylinder and cone composites in every dimension, type-checked and exportable to path types.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Finster and Mimram's type theory Catt provides the framework for the whole paper; uniqueness of derivations justifies the mutual recursion on derivation trees.","marker":"[24]"},{"why":"Benjamin's thesis supplies the depth-0 functoriality case, the lemmas that a functorialised pasting context is again pasting and that promoted types stay full, and the d = k = 0 part of the proof.","marker":"[10]"},{"why":"Benjamin and Markakis supply the reduction of pasting contexts (Section 4.4) and the reduction substitution on which the general-composite case and Lemma B.21 depend; the theorem is cited, not reproved.","marker":"[13]"},{"why":"Dean et al.'s characterisation of variables of the source and target of a computad is used in Lemma B.5 to locate depth-0 variables in the boundary, needed for the reduced-composite interchangers.","marker":"[23]"},{"why":"Batanin's account of pasting contexts as rooted planar trees supplies the composition operation on pasting contexts used to build the interchanger coherences.","marker":"[8]"},{"why":"Benjamin's export mechanism converts Catt terms into functions computing inhabitants of identity types in homotopy type theory, giving the claimed transfer of all examples to path types.","marker":"[11]"}],"fun_headline_variants":["Recursive naturality builds cylinders and cones in omega-categories","Machine-checked naturality for higher paths in omega-categories","One meta-operation yields naturality for weak omega-categories","Naturality via recursion: cylinders and cones for all dimensions"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Recursive naturality builds cylinders and cones in omega-categories","Machine-checked naturality for higher paths in omega-categories","One meta-operation yields naturality for weak omega-categories","Naturality via recursion: cylinders and cones for all dimensions"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000543,"raw_usage":{"total_tokens":2586,"prompt_tokens":919,"completion_tokens":1667,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":535,"completion_tokens_details":{"reasoning_tokens":1598}},"tokens_in":535,"tokens_out":1667,"duration_ms":14111,"temperature":1.0,"reasoning_tokens":1598,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T18:04:09.467592+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"‘A type theoretic approach to weak ω-categories and related higher structures’","cited_arxiv_id":null,"evidence_quote":"Benjamin's thesis supplies the depth-0 functoriality case, the lemmas that a functorialised pasting context is again pasting and that promoted types stay full, and the d = k = 0 part of the proof."},{"cited_title":"‘Invertible cells in ω-categories’","cited_arxiv_id":null,"evidence_quote":"Benjamin and Markakis supply the reduction of pasting contexts (Section 4.4) and the reduction substitution on which the general-composite case and Lemma B.21 depend; the theorem is cited, not reproved."},{"cited_title":"Generating Higher Identity Proofs in Homotopy Type Theory","cited_arxiv_id":"2412.01667","evidence_quote":"Benjamin's export mechanism converts Catt terms into functions computing inhabitants of identity types in homotopy type theory, giving the claimed transfer of all examples to path types."}],"review_version":1}