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)\to \mathcal{B}$ for contextual categories ${\mathcal{A}}_i$, $\mathcal{B}$, and describe a bijective correspondence between bimorphisms $(\mathcal{A},\mathcal{B})\to \mathcal{C}$ and morphisms $\mathcal{A}\to {\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})\to \mathcal{C}$ are in natural bijection with morphisms $\mathcal{A}\otimes \mathcal{B}\to \mathcal{C}$. We extend $\otimes :\text{Cont}\times \text{Cont}\to \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.

80 pages