Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

A monoidal category of dependently sorted algebraic theories I: syntax

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

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

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2511.13547 v2 pith:O2WX4YXL submitted 2025-11-17 math.CT math.LO

Daniel Almeida This is my paper · ORCID
classification math.CTmath.LO MSC 18C1018M0503G30
keywords generalizedalgebraictheoriesdependentsortstensorproductofmonoidalcategorycontextualcategoriesheightfunctiondisplayedstructurestypetheory
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'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.

What carries the argument

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

What would settle it

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.

Watch

Extended reading notes

Core claim

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

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
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.

Referee Report

3 major / 5 minor

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.

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 (3)
  1. [§5, Proposition 5.1 (case analysis)] 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.
  2. [§5, term⊙term case (3)] 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.
  3. [§3.3, D(S⊗T)≅D(S)×D(T)] 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.
minor comments (5)
  1. [§4, proof of Sub1_t,t(h)] In the displayed assumption, 'H(f∶X→A)ht(Y⊢vterm)' should read 'ht(f∶X→A)ht(Y⊢vterm)'.
  2. [§5, sort⊙term equality case (8)] 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)'.
  3. [§3.1.3] 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'.
  4. [§2.1.2] 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.
  5. [§7–§8] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the tensor-product derivability theorem is proved by an internal induction on a height function; deferred sequel claims are not load-bearing.

full rationale

The paper's central claim, Theorem 5.2, is that J⊙J′ is derivable in the pretheory A⊗B for any derivable judgments J and J′, so that A⊗B is a theory. This is established in Section 5 by induction on ht(J)·ht(J′): Proposition 5.1 proves (h+1)-derivability from h-derivability, and the recursive clauses of ⊗_t and ●_t are shown to appeal only to products of strictly lower height via Proposition A.15. The height function is built on a modified inference system whose equivalence with Cartmell's system is proved in the appendix (Prop. A.21), not assumed. The construction is therefore self-contained: the input (axioms and derivability in A and B) is used through the height inequalities, not through the desired conclusion. The paper's own caveats — e.g. that the height choice is made for a 'technical reason which, I believe, is unessential,' and that functoriality, universal properties, and the monoidal structure are deferred to [Alm26] — are explicitly non-load-bearing for Theorem 5.2, since [Alm26] is never used as a premise in the proof. No fitted parameter is renamed as a prediction, no defining equation identifies the conclusion with an input, and no uniqueness theorem is imported from the authors' earlier work. Several verifications are said to be 'analogous,' 'sketched,' or 'omitted' (e.g. the t-sub case in term⊙term, parts of associativity, and parts of the symmetry proof); these are correctness/completeness concerns about the write-up, not circular reductions. In particular, the 'term⊙sort equality' case that a reader might worry is absent is in fact treated in Section 5 under that heading, so even that possible gap is not a circular step.

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

No numbers are fitted to data and no empirical constants appear; the only choice-like inputs are structural (chosen variables outside contexts, lexicographic matrix order, the particular height function), which the paper argues do not affect the resulting equivalence classes of theories. The new syntactic forms (S,T), (s,T), (S,t) and the tensor contexts X⊗Y are outputs of the algorithm whose existence is certified by Theorem 5.2, not unexplained postulates; hence no invented entities, in the graviton-problem sense, are needed.

assumptions (5)
  • domain assumption Cartmell's framework for generalized algebraic theories and the equivalence GAT ≃ Cont between gats and contextual categories.
    Definitions of pretheory, theory, judgment, and the interpretation of the tensor product as a presentation of C(A)⊗C(B) are taken from Cartmell [Car78; Car86] (§1, §6, Appendix A).
  • domain assumption The modified inference rules of the appendix induce exactly the same derivable judgments as Cartmell's rules (Prop. A.21).
    All heights and the h-derivability induction in §4–§5 are relative to the appendix's rule system; the paper proves the equivalence, but the central proofs depend structurally on this premise.
  • domain assumption Height-function inequalities of Prop. A.15 (strict decrease on subterms/subcontexts) hold.
    The recursion for ⊗_t, ●_t and the inductions Cont(k)/Sub/Mor all use ht(X⊢s_i) < ht(X⊢S(…)) etc.; the paper proves these, but they are load-bearing for the termination and induction arguments.
  • ad hoc to paper Each context carries a chosen variable not contained in it (choice function).
    Footnote 8: this choice is required for the operations to be defined; the paper argues different choices yield equal-up-to-renaming theories, so it is non-essential.
  • domain assumption Lee's correspondence between type signatures and locally finite direct categories (PSh_fp(D)), used in §3.3.
    The lfdc example and the claimed D(S⊗T)≅D(S)×D(T) rely on Lee21 Chapter 1; Lemma 3.3's characterization also states "we have omitted the details".

how reviews work

0 comments
Cite this review

Pith. "Pith review of A monoidal category of dependently sorted algebraic theories I: syntax." pith.science (2026). https://pith.science/paper/O2WX4YXL

@misc{pith2026251113547,
  author       = {Pith},
  title        = {Pith review of: A monoidal category of dependently sorted algebraic theories I: syntax},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/O2WX4YXL}},
  note         = {Machine review of arXiv:2511.13547}
}
abstract

This is the first of a pair of papers where we construct and investigate a closed monoidal structure on the category of generalized algebraic theories (in the sense of Cartmell). In the present text, as a starting point, we define the tensor product, $A \otimes B$, between two generalized algebraic theories $A$ and $B$. This is done syntactically via an algorithm that uses the axioms of $A$ and $B$ in a recursive manner to produce those of $A \otimes B$. We provide examples of known structures that are recovered by our construction, such as tensor products of Lawvere theories, "cellular" products of dependent type signatures, and theories of diagrams and of displayed structures. It will be verified in the second volume that, as suggested by these special cases, the category of family-valued models $\text{Mod}(A \otimes B,\text{Fam})$ is isomorphic to $\text{Mod}(A,\textbf{Mod}(B))$ and to $\text{Mod}(B,\textbf{Mod}(A))$ for certain contextual categories $\textbf{Mod}(A)$ and $\textbf{Mod}(B)$ whose underlying categories are equivalent to $\text{Mod}(A,\text{Fam})$ and to $\text{Mod}(B,\text{Fam})$, respectively. Moreover, the cellular structure of the tensor product is obtained by combining, via a pushout-product operation, those of the two theories. We also construct a functor $\otimes_{A,B}:\mathcal C(A) \times \mathcal C(B) \rightarrow \mathcal C(A \otimes B)$ comparing the associated contextual categories, and describe isomorphisms of the forms $(A \otimes B) \otimes C \cong A \otimes (B \otimes C)$ and $A \otimes B \cong B \otimes A$. In the sequel paper we will describe a universal property of $\otimes_{A,B}$, which will induce functoriality of the tensor product and thus allow us to check the monoidal category conditions.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A monoidal category of dependently sorted algebraic theories II: categorical aspects

    math.CT 2026-05 unverdicted novelty 6.0 of 10

    Constructs the exponential A^B and proves existence of tensor A ⊗ B on contextual categories such that bimorphisms correspond to morphisms from the tensor, extending to a closed symmetric monoidal structure on Cont.

Reference graph

Works this paper leans on

7 extracted references · 1 canonical work pages · cited by 1 Pith paper

  1. [79]

    Algebra valued functors in general and tensor products in particular

    [Fre66] P . Freyd. “Algebra valued functors in general and tensor products in particular”. In:Colloq. Math. 14 (1966), pp. 89–106.ISSN: 0010-1354,1730-6302.DOI:10.4064/cm- 14- 1- 89- 106.URL:https: //doi.org/10.4064/cm-14-1-89-106. [Fre72] Peter Freyd. “Aspect of topoi”. In:Bull. Austral. Math. Soc.7 (1972), pp. 1–76.ISSN: 0004-9727. DOI:10.1017/S00049727...

    doi:10.4064/cm- 1966

  2. [104]

    The theory and practice of Reedy categories

    Contemporary Mathematics. Providence, RI: American Mathematical Society, 1989, pp. viii+176. ISBN: 0-8218-5111-X.DOI:10.1090/conm/104. [RieVer14] Emily Riehl and Dominic Verity. “The theory and practice of Reedy categories”. In:Theory Appl. Categ.29 (2014), pp. 256–301.ISSN: 1201-561X. 119

    doi:10.1090/conm/104 1989

  3. [189]

    The logic of structures

    London Mathe- matical Society Lecture Note Series. Cambridge University Press, Cambridge, 1994, pp. xiv+316. ISBN: 0-521-42261-2.DOI:10 . 1017 / CBO9780511600579.URL:https : / / doi . org / 10 . 1017 / CBO9780511600579. [Age92] Pierre Ageron. “The logic of structures”. In:J. Pure Appl. Algebra79.1 (1992), pp. 15–34.ISSN: 0022- 4049,1873-1376.DOI:10.1016/0...

    work page doi:10.1016/0022-4049(92)90123-w.url:https://doi.org/10.1016/0022- 1994

  4. [221]

    Algebraic models of homotopy types and the homotopy hypothesis

    Lecture Notes in Mathematics. Springer-Verlag, Berlin-New York, 1971, pp. v+200. [Hen16] Simon Henry. “Algebraic models of homotopy types and the homotopy hypothesis”. In: (2016). arXiv:1609.04622 [math.CT].URL:https://arxiv.org/abs/1609.04622. [Kel82] G. M. Kelly. “Basic concepts of enriched category theory”. In:Repr. Theory Appl. Categ.10 (2005). Reprin...

    arXiv 1971

  5. [1978]

    Generalised algebraic theories and contextual categories

    [Car86] John Cartmell. “Generalised algebraic theories and contextual categories”. In:Ann. Pure Appl. Logic32.3 (1986), pp. 209–243.ISSN: 0168-0072,1873-2461.DOI:10.1016/0168-0072(86)90053-9. URL:https://doi.org/10.1016/0168-0072(86)90053-9. [Ehr68] Charles Ehresmann. “Esquisses et types des structures alg ´ebriques”. In:Bul. Inst. Politehn. Ia¸ si (N.S.)...

    doi:10.1016/0168-0072(86)90053-9 1986

  6. [2000]

    Multilinearity of sketches

    [Ben97] David B. Benson. “Multilinearity of sketches”. In:Theory Appl. Categ.3 (1997), No. 11, 269–277. ISSN: 1201-561X. [Bir84] Gregory J. Bird. “Limits in 2-categories of locally-presented categories”. PhD thesis. University of Sydney,

    1997

  7. [2020]

    Homotopy Languages

    arXiv:2004.12937 [math.CT].URL:https://arxiv.org/abs/2004.12937. [BarHen25] C ´esar Bardomiano Mart´ınez and Simon Henry. “Homotopy Languages”. In: (2025). arXiv:2510. 02607 [math.CT].URL:https://arxiv.org/abs/2510.02607. [BasEhr72] Andr ´ee Bastiani and Charles Ehresmann. “Categories of sketched structures”. In:Cahiers Topolo- gie G´ eom. Diff´ erentiell...

    arXiv 2004

Pith tools

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