{"id":"5d039485-7b8d-40eb-9384-6b89b867a1a5","arxiv_id":"2511.13547","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A tensor product of generalized algebraic theories (Cartmell-style dependent type theories) is constructed syntactically and proved to yield a theory, recovering Lawvere tensor products, double categories, diagrams, and displayed structures as special cases.","lead":"This paper defines a way to combine two algebraic theories with dependent types into a single \"joint\" theory, extending Lawvere and Freyd's 1960s tensor product to dependent type theories. The sequel promises that models of the combined theory are exactly pairs of compatible models, yielding a toolbox for structures such as double categories and displayed categories.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition 5.1 omits the term⊙sort-equality case, so Theorem 5.2 is not proven for term axioms tensored with sort-equality axioms.","rationale":"Read in good faith: the paper's construction is intricate, and much of the machinery (height function, modified rules) is plausibly sound. The reader's CONDITIONAL verdict captures the general risk around the height function. My pass found a more specific, checkable gap: the proof of Prop 5.1 lacks the term⊙sort-equality case. Since Theorem 5.2 is the paper's central claim, and its proof is by an exhaustive case analysis on judgment kinds, a missing case means the theorem is not established as written. This is not an accusation of fraud; it is a structural omission that a careful proof must fill. The concrete test—completing the case—would settle whether the gap is benign. I therefore keep the reader's CONDITIONAL verdict (UNCHANGED), while sharpening the reason: not just 'height machinery unverified' but a specific unproved case in the main induction. Agreement with the reader is partial: their weakest_assumption concerned Prop A.15/A.21; mine is a missing case that relies on those same height inequalities.","tokens_in":88162,"tokens_out":9549,"duration_ms":90146,"concrete_test":"Write out the omitted term⊙sort-equality case of Prop 5.1: for J = (X⊢u:U) and J′ = (Y⊢V≡V′ sort), derive X⊗Y′ ⊢ u⊗y_V ≡ u⊗y_{V′} : (U⊗V)[...] using the pattern of the 'sort⊙term equality' proof but with Sub2_* lemmas and Conteq2/Moreq2. Check that every intermediate judgment has ht(J₁)ht(J₂) ≤ h via Prop A.15. If this derivation cannot be completed, Theorem 5.2 is unsupported. A stronger version: machine-check the whole of Prop 5.1 to force all omitted cases.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 5's proof of Proposition 5.1 (h-derivability ⇒ (h+1)-derivability) does not cover the case where J is a term judgment and J′ is a sort equality judgment. This case is defined in §2.2 ('term⊙sort equality') and required by Table 1 (Term ⊗ Sort-eq → Term eq). The surrounding cases sort⊙term-equality and term-equality⊙sort are proven, but they use the one-sided Sub1/Sub2 lemmas respectively; the construction is not symmetric, and the paper does not state that the missing case is analogous. Theorem 5.2 concludes A⊗B is a theory by applying Prop 5.1 to all axioms; axioms include J⊙J′ for J a term axiom in A and J′ a sort-equality axiom in B. Without this case, the induction does not establish that these axioms are well-formed. The paper explicitly omits some verifications (e.g. the t-sub case in term⊙term), but a top-level case is missing here. If the missing case cannot be derived from the h-derivability hypotheses and Prop A.15 height inequalities, the main theorem collapses.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines a syntactic tensor product A⊗B of generalized algebraic theories (Cartmell gats). The alphabet of A⊗B has pairs of sorts, and terms of the forms (s,T) and (S,t). A recursive algorithm combines derivable judgments J in A and J' in B into judgments J⊙J' according to Table 1, and A⊗B is the pretheory whose axioms are all such combinations of axioms. The central theorem (Theorem 5.2) asserts that every pair of gats is h-derivable for all h, hence that A⊗B is a genuine theory. The proof is organized as an induction on ht(J)·ht(J') using a modified derivation system and a height function developed in the appendix. The paper also constructs a comparison functor C(A)×C(B)→C(A⊗B), recovers known tensor products (Lawvere theories, cellular products, theories of diagrams and displayed structures), and sketches associativity and symmetry isomorphisms, with full functoriality and universal properties deferred to a sequel. The text itself repeatedly records omitted verifications: in §3.3, in the term⊙term case of §5, and throughout the sketches in §§7–8.","tokens_in":88261,"tokens_out":6773,"duration_ms":71466,"significance":"If the main theorem is correct, this is a substantial and original contribution: it provides the first syntactic tensor product for generalized algebraic theories, with a genuinely non-trivial proof mechanism (the modified inference rules and height function). The construction is well-motivated and the examples are informative, connecting the tensor product to Freyd's tensor product of Lawvere theories, to Leibniz/pushout-product structures in presheaf categories, and to the theories of diagrams and displayed structures. The paper is self-contained in the sense that the key derivability theorem is proved internally rather than imported from the author's earlier work. However, the main theorem is currently not fully proved: one top-level case in Proposition 5.1 (term judgment tensored with sort-equality judgment) is absent, and another asymmetric subcase is explicitly left out. These omissions are load-bearing for Theorem 5.2, so the central claim is not yet established as written.","major_comments":[{"comment":"The proof of Proposition 5.1 does not treat the case where J is a term judgment and J' is a sort equality judgment. This case is defined in §2.2 ('term⊙sort equality') and required by Table 1: it produces a term-equality judgment, and in particular a term-equality axiom for every pair consisting of a term axiom of A and a sort-equality axiom of B. The surrounding cases 'sort⊙term equality' and 'term equality⊙sort' are proved, but the recursive definitions of ⊗_t and ●_t in §2.1.1 are not symmetric, and no reduction of the missing case to the proved ones is indicated. Without this case, the induction in Theorem 5.2 does not establish well-formedness of all axioms of A⊗B, so the conclusion that A⊗B is a theory is unsupported when B has sort equality axioms.","section":"§5, Proposition 5.1 (case analysis)"},{"comment":"In the term⊙term case, the proof handles J having an initial inference of the form (t-sub) in case (2), but for J' having an initial inference (t-sub) it says only that the verification 'has been omitted' and is analogous. This is an asymmetric case: substitution in the second factor requires the Sub2-type statements rather than the Sub1-type statements used in case (2). Since Proposition 5.1 is quantified over all derivable judgments, an omitted subcase in this case analysis breaks the induction for h-derivability. The full verification, or a formal reduction to the symmetric situation, is needed.","section":"§5, term⊙term case (3)"},{"comment":"The proof of the claimed isomorphism for locally finite direct categories ends with '(Details have been omitted.)' at the limit step of the well-founded induction. This section is advertised in the introduction as recovering the cellular product of dependent type signatures, so this is a substantive claim rather than a remark. Either supply the missing colimit argument or explicitly label the statement as a conjecture/outline.","section":"§3.3, D(S⊗T)≅D(S)×D(T)"}],"minor_comments":[{"comment":"In the displayed assumption, 'H(f∶X→A)ht(Y⊢vterm)' should read 'ht(f∶X→A)ht(Y⊢vterm)'.","section":"§4, proof of Sub1_t,t(h)"},{"comment":"The judgment 'Mor2_s,t(h)' appears where the context is X⊗f and the conclusion concerns substituting a term of B; this looks like a typo for 'Sub2_s,t(h)'.","section":"§5, sort⊙term equality case (8)"},{"comment":"The text says 'one in which squares compose vertically (having horizontal arrows are their sources/targets), and one where they compose vertically'; the second should presumably be 'compose horizontally'.","section":"§3.1.3"},{"comment":"The domain of ⊗_s is written as Der^+_s(A)⊗Der^+_s(B), but a Cartesian product is meant; the tensor notation is potentially confusing.","section":"§2.1.2"},{"comment":"Sections 7 and 8 are explicitly labelled as sketches and the paper states that the categorical study is deferred to [Alm26]. The abstract's wording 'describe isomorphisms' should be aligned with the proof status: as written, these results are only outlined.","section":"§7–§8"}],"recommendation":"major_revision","confidential_remarks":"The missing term⊙sort equality case in §5 is the most serious obstacle: it directly affects the induction proving Theorem 5.2. If it cannot be supplied, the central claim collapses; if it can, the rest of the paper is likely salvageable with a careful revision. The omitted t-sub subcase in term⊙term and the omitted details in §3.3 should also be completed or clearly downgraded."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Daniel Almeida has pulled off something real: a syntactic tensor product for Cartmell's generalized algebraic theories, with a proof that the result is a theory. The construction is genuinely new as far as I can tell—Freyd/Kelly cover Lawvere/enriched theories, Lee covers type signatures, and the sketch tensor products don't handle dependent sorts. The examples are worth the price of admission: tensoring the theory of categories with itself gives strict double categories, and the displayed-structure example (E⊗T_cat) matches Ahrens–Lumsdaine. The comparison functor in §6 is also constructed cleanly.\n\nThe main proof is a big induction on a height function, and the paper openly replaces Cartmell's derivation rules to get the needed height inequalities (App. A). That's a lot of machinery, but the organization is careful and the paper explicitly lists what it is not proving.\n\nThe soft spots are real but not fatal on their own. The paper omits several verifications: §3.3 says 'details have been omitted'; §5 omits the t-sub case in term⊙term; §§7-8 are sketches. More seriously, the stress-test case appears to hold up: Proposition 5.1 never treats the term⊙sort-equality case, which Table 1 says should produce a term equality. The surrounding cases sort-equality⊙term and term⊙sort are handled, but the construction is asymmetric, so 'analogous' is not automatic. Since Theorem 5.2 concludes A⊗B is a theory by applying Prop 5.1 to all pairs of axioms, this missing case is load-bearing. It may well be derivable by the same height induction—I don't see an obvious obstruction—but as written the proof has a hole.\n\nThe paper deserves a serious referee. It's a first paper of a pair and the author is up front about deferring functoriality and universal properties. The missing case needs to be closed, and the referee should check whether the height machinery is actually sound. I would engage with it.","headline":"A genuinely new tensor product for gats with a real proof gap: the term⊗sort-equality case is missing from Proposition 5.1, so Theorem 5.2 is not fully proven as written.","tokens_in":88921,"tokens_out":3650,"would_cite":true,"duration_ms":35795,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18C10","18M05","03G30"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper constructs a tensor product A⊗B of any two generalized algebraic theories and proves, by a height-based induction, that the syntactic algorithm always yields a well-formed theory.","keywords":["generalized algebraic theories","dependent sorts","tensor product of theories","monoidal category","contextual categories","height function","displayed structures","dependent type theory"],"falsifier":"Find a generalized algebraic theory with a derivable sort judgment X⊢S(s_1,…,s_k) sort such that, under the appendix's modified rules, the height of some premise X⊢s_i∶U is not strictly smaller than the height of the conclusion; this would falsify Proposition A.15, the inequality on which every induction step in Sections 4–5 depends.","tokens_in":87839,"feed_emoji":"🔗","tokens_out":12581,"duration_ms":108553,"temperature":0.7,"pith_summary":"The paper's central claim is that any two generalized algebraic theories—dependent-sorted algebraic theories of the kind used in dependent type theory—can be combined into a third theory A⊗B by a purely syntactic recipe. The recipe pairs sort symbols, creates two kinds of term symbols from the two factors, and combines each axiom of A with each axiom of B; the difficulty is to prove the recursive procedure terminates and that every resulting judgment is well-formed. This is achieved in Theorem 5.2 by proving a stronger statement: for any pair of derivable judgments, their 'tensor' is derivable, using induction on the product of their heights. A sympathetic reader should care because a tensor product is precisely what turns these theories into a monoidal category, with models of A⊗B being models of A inside models of B; the construction unifies the classical tensor product of single-sorted equational theories, cellular products of dependent type signatures, and theories of diagrams and displayed structures. The paper also constructs the comparison functor between syntactic categories and records that the tensor product is associative and symmetric.","feed_headline":"Dependent-sorted theories combine: A⊗B is always a theory","feed_subtitle":"Recursive merging of axioms yields a tensor product of dependent theories, unifying equational and displayed structures.","key_machinery":"The load-bearing device is the recursive definition of the two tensor-term operations ⊗_t and ●_t, which implement the two orders of applying an operation of A and an operation of B to a matrix of variables (column-first versus row-first); in the single-sorted case these are the two sides of the classical interchange axiom f(g(x_ij)) = g(f(x_ij)). A sort-tensor operation ⊗_s builds the sort symbol (S,T) with boundary computed by the Leibniz formula ∂(X⊗Y) = ∂X⊗Y ×_{∂X⊗∂Y} X⊗∂Y. Around this, the essential machinery is the height function and the 'h-derivability' bootstrap: Section 4 builds consequences (contexts, substitutions, morphisms) under an h-derivability assumption, and Section 5 uses","core_discovery":"The central discovery is Theorem 5.2: for any generalized algebraic theories A and B, the pair (A,B) is h-derivable for every h≥0, meaning every tensor J⊙J' of derivable judgments is derivable; in particular the pretheory A⊗B—whose axioms are the tensors of axioms—is a genuine generalized algebraic theory rather than merely a pretheory. The proof introduces a modified inference system equivalent to the standard one, with a height function ht on judgments that is strictly increasing along subterm constructions, and then proves a bootstrap: h-derivability implies (h+1)-derivability, using a battery of substitution and morphism lemmas established for height-product ≤h. This makes precise the cl","pith_inferences":["If the tensor product is a genuine monoidal product, the category of generalized algebraic theories itself becomes a model of multiplicative linear logic: a theory A*B would combine the structure of two dependent theories with an internal hom B^A expressing a theory of morphisms of A-models; the paper states that the monoidal/categorical verification is deferred to a sequel.","The h-derivability hierarchy suggests a measure of 'interaction depth' between two theories: one could define h-tensor products that only combine judgments up to height product h, interpolating between the disjoint union and the full tensor. This extension is not in the paper.","The Leibniz formula for the sort-only case points the way to a model-theoretic reading: if Mod(A⊗B) ≃ Mod(A)⊗Mod(B) holds under appropriate conditions (which the paper flags as subtle and only conditionally expected), then the tensor product would be the monoidal product of locally presentable categories equipped with their cofibrantly generated weak factorization systems—matching the intuition of","Since the construction is explicit, it offers a termination-based test for the joint consistency of two dependently-sorted theories: the algorithm of §2 either produces a well-formed theory or fails after finitely many steps; the paper's theorem says it never fails."],"forward_implications":["If A⊗B is a theory, then the category of family-valued models of A⊗B is isomorphic to the category of A-models inside B-models and to B-models inside A-models (stated as the sequel's theorem).","The construction reproduces the classical tensor product of single-sorted equational theories, with the interchange axiom t(s(x_ij)) = s(t(x_ij)).","For the sort-only (type-signature) case, the tensor product yields the cellular product with boundary ∂(X⊗Y) = ∂X⊗Y ×_{∂X⊗∂Y} X⊗∂Y, so X⊗Y has length ℓ(X)ℓ(Y).","The interval theory I gives a theory of morphisms I⊗A, and the display theory E gives a theory of displayed structures E⊗A for any theory A.","The tensor product is associative and symmetric: (A⊗B)⊗C and A⊗(B⊗C) have the same derivable judgments, and A⊗B ≅ B⊗A."],"fun_headline_variants":["A⊗B always a theory: dependent-sorted syntax merges","Tensor product of dependent theories proven genuine","Dependent theories combine: new tensor product syntax"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The proof leans on the appendix's modified derivation rules having both the height inequalities of Proposition A.15 and exactly the same derivable judgments as the standard rules (Proposition A.21); if either property fails, the height induction behind Theorem 5.2 collapses.","fun_headline_variants_meta":{"raw":{"variants":["A⊗B always a theory: dependent-sorted syntax merges","Tensor product of dependent theories proven genuine","Dependent theories combine: new tensor product syntax"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000278,"raw_usage":{"total_tokens":1583,"prompt_tokens":926,"completion_tokens":657,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":670,"completion_tokens_details":{"reasoning_tokens":608}},"tokens_in":670,"tokens_out":657,"duration_ms":7605,"temperature":1.0,"reasoning_tokens":608,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-03T21:45:57.418137+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find a generalized algebraic theory with a derivable sort judgment X⊢S(s_1,…,s_k) sort such that, under the appendix's modified rules, the height of some premise X⊢s_i∶U is not strictly smaller than the height of the conclusion; this would falsify Proposition A.15, the inequality on which every induction step in Sections 4–5 depends.","supporting_citations":[],"review_version":1}