Proposition 3.5: universal property of the free algebra

Fix a type $S$ whose elements are called sorts (it lives in the lowest type universe; no finiteness is assumed of it). The statement takes the following parameters:

• a signature $\mathrm{sig}$: for every finite list of sorts $w=[s_1,\dots,s_k]$ and every sort $s$, a type $\mathrm{sig}(w,s)$ whose elements are operation symbols of input arity $w$ and output sort $s$ (no finiteness assumed);
• a sorted set of variables $X$: for each sort $s$, a type $X_s$;
• an algebra $A$ for $\mathrm{sig}$: a carrier family $(A_s)_{s\in S}$ of types, together with, for every $w=[s_1,\dots,s_k]$, every $s$, and every symbol $\sigma\in\mathrm{sig}(w,s)$, an interpretation $\sigma^A:A_{s_1}\times\cdots\times A_{s_k}\to A_s$ (when $k=0$ the domain is a one-point type, so $\sigma^A$ names a constant of $A_s$);
• a variable assignment $\rho$: a family of functions $\rho_s:X_s\to A_s$, one per sort $s$.

From $\mathrm{sig}$ and $X$ one builds the term algebra $T=\mathrm{freeAlgebra}(\mathrm{sig},X)$: its carrier at sort $s$ is the inductive type $\mathrm{Term}_s$ of well-sorted terms, generated by a constructor $\mathrm{var}:X_s\to\mathrm{Term}_s$ and a constructor that, from a symbol $\sigma\in\mathrm{sig}(w,s)$ and a tuple of subterms whose sorts match $w$, forms a term of sort $s$; the operation $\sigma^{T}$ sends a tuple of terms to the formal term $\sigma$ applied to them. The map $\eta$ is the family $\eta_s:X_s\to\mathrm{Term}_s$ given by $\eta_s(x)=\mathrm{var}(x)$. A homomorphism $g:T\to A$ consists of a family of functions $g_s:\mathrm{Term}_s\to A_s$ such that for all $w=[s_1,\dots,s_k]$, all $s$, all $\sigma\in\mathrm{sig}(w,s)$, and all argument tuples $(t_1,\dots,t_k)$,

i.e. $g$ commutes with every operation, applied componentwise to arguments.

The theorem asserts that there exists exactly one homomorphism $g:T\to A$ satisfying

equivalently $g_s(\mathrm{var}(x))=\rho_s(x)$ for every sort $s$ and every $x\in X_s$. The "$\exists!$" means: such a homomorphism exists, and any two homomorphisms both satisfying this variable-agreement condition are equal (equality of the homomorphism structures, which reduces to equality of the underlying function families, the commutation law being a proposition). Degenerate cases falling under the quantifiers: if $S$ is empty, or if $X_s$ is empty for every sort $s$, the agreement condition on $g$ is vacuous and the claim becomes that there is exactly one homomorphism $T\to A$ at all; nullary symbols ($w=[]$) are included, their argument tuple being the unique element of a one-point type.