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

Abstract

This is the second 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). Having presented the tensor product of theories in a syntactic way, we now study the same structure from the perspective of contextual categories. We define the exponential $\mathcal A^\mathcal B$ between two contextual categories $\mathcal A$, $\mathcal B$, and show how this yields, as a particular case, a cotensor $\mathcal A^B$ by a small category $B$. We also introduce a concept of multimorphism $(\mathcal A_1, ..., \mathcal A_n) \rightarrow \mathcal B$ for contextual categories $\mathcal A_i$, $\mathcal B$, and describe a bijective correspondence between bimorphisms $(\mathcal A, \mathcal B) \rightarrow \mathcal C$ and morphisms $\mathcal A \rightarrow \mathcal C^\mathcal B$. We give an abstract proof that there exists a contextual category $\mathcal A \otimes \mathcal B$ such that bimorphisms $(\mathcal A, \mathcal B) \rightarrow \mathcal C$ are in natural bijection with morphisms $\mathcal A \otimes \mathcal B \rightarrow \mathcal C$. We extend $\otimes:\text{Cont} \times \text{Cont} \rightarrow \text{Cont}$ into a closed symmetric monoidal structure and give a description of certain pushout-tensor maps that, in particular, allows us to prove that the tensor product of theories from part I is functorial and presents the one constructed here.