Fix a finitary algebraic theory $\mathrm{𝒯︀}$: sorts $𝑆$, a signature $𝜎$, equations, and a set $𝑉$ of generators. Write $𝑴$ for the free $\mathrm{𝒯︀}$-model on $𝑉$ and $|𝑴{|}_{𝑠}$ for its carrier at sort $𝑠$.

A $\mathrm{𝒯︀}$-type of sort $𝑠$ is a family $𝐴:|𝑴{|}_{𝑠}\to \text{𝖳𝗒𝗉𝖾}$.

For $\mathrm{𝒯︀}$-types $𝐴$ and $𝐵$ of sort $𝑠$ we have the additives, defined pointwise,

along with $\top$, $\perp$, and their indexed versions.

Each operation $𝑜:{𝑠}_0,\dots ,{𝑠}_{𝑛-1}\to 𝑠$ of $\mathrm{𝒯︀}$ gives a multiplicative, defined by Day convolution,

Each lifted operation also has closed structure: a residual in each of its arguments. Day algebras [1] give a more general convolutional definition.

When $\mathrm{𝒯︀}$ is the theory of monoids and $𝑉$ is an alphabet, $\mathrm{𝒯︀}$-types are formal grammars. Multiplication gives $\otimes$, the unit gives $𝜀$, and we recover Lambek${\begin{array}{}\end{array}}^{𝙳}$.