A monoidal category of dependently sorted algebraic theories I: syntax

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.