A monoidal category of dependently sorted algebraic theories I: syntax
Daniel Almeida
TL;DR
This work develops a syntactic construction of the tensor product of generalized algebraic theories, yielding a framework in which a closed monoidal structure on Gat and an induced enrichment on contextual categories can be studied. By defining tensor expressions from pairs of judgments and assembling a pretheory whose axioms are tensorized cross-axioms, the authors connect syntactic manipulation with semantic notions like two-sided substitution and display maps. They establish height-based inductive arguments (h-derivability) to prove that A ⊗ B is indeed a theory and to derive a two-sided functorial correspondence between contextual categories, paving the way for a monoidal and Cat-enriched structure. Examples, including strict double categories and Lawvere theories, illustrate how familiar constructions arise as instances of their tensor product, and preliminary symmetry/associativity results indicate a robust monoidal structure, with the full monoidal framework and universal properties to be developed in a sequel. Collectively, the paper provides explicit, computable recipes for tensoring theories, linking syntactic presentations to enriched categorical semantics.
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.