The Azimuth Project
Multi-sorted algebraic theory


A multi-sorted algebraic theory generalizes the notion of a Lawvere theory.


We give the definition found in Rigidification of algebras over multi-sorted theories. We don’t know where it is first given.

Definition. Given a set SS, an SS-sorted algebraic theory 𝒯\mathcal{T} is a small category with objects T α n̲T_{\underline{\alpha^n}} where α n̲=α 1,,α n\underline{\alpha^n} = \langle \alpha_1, \dots, \alpha_n \rangle for α iS\alpha_i \in S and n0n \geq 0 varying, and such that each T α n̲T_{\underline{\alpha^n}} is equipped with an isomorphism T α n̲ i=1 nT α iT_{\underline{\alpha^n}} \cong \prod_{i=1}^n T_{\alpha_i}.