nLab
tensor product theory

If AA and BB are algebraic theories, the algebraic theory ABA\otimes B is characterized by the fact that its models can be identified with AA-models in BModB Mod, or equivalently as BB-models in AModA Mod. There are maps of theories AABA\to A\otimes B and BABB\to A\otimes B which are universal for maps of theories ACA\to C and BCB\to C whose images commute, for any theory CC.