Lawvere Theory

A Lawvere theory is a categorical encoding of the substitution calculus of a single-sorted algebraic theory. There are some subtleties due to strictness, but the traditional definition is that a Lawvere theory is a category 𝒯 𝒯 \mathcal{T} equipped with an Identity-On-Objects Functor, strictly product-preserving functor A : 𝔽 m ⁢ a ⁢ t ⁢ h ⁢ r ⁢ m ⁢ o ⁢ p → T : 𝐴 → superscript 𝔽 𝑚 𝑎 𝑡 ℎ 𝑟 𝑚 𝑜 𝑝 𝑇 A:\mathbb{F}^{mathrm{op}}\to T from the Opposite Category of the Category of Standard Finite Sets.