Congruence formations yield regular-language formations

For every implicitly quantified type of sorts $S$ equipped with a typeclass witness that $S$ is finite (with $S=\varnothing$ allowed), every implicitly quantified $S$-sorted signature $\Sigma$—meaning that for each finite list $w$ of input sorts and each output sort $s$, $\Sigma(w,s)$ is an arbitrary type of operation symbols, with no finiteness or nonemptiness assumption—and every finite-index congruence formation $F$ for $\Sigma$, there exists a regular-language formation $\mathcal L$ for $\Sigma$, not asserted to be unique, such that for every $S$-indexed family of types $X=(X_s)_{s\in S}$, including families having empty or infinite components, the selected languages are exactly $\mathcal L(X)=\{K\mid \exists\Phi,\ \Phi\in F(X)\ \text{and}\ \forall s\,\forall x,y\in T_\Sigma(X)_s,\ x\mathrel{\Phi_s}y\Rightarrow(x\in K_s\leftrightarrow y\in K_s)\}$, where $T_\Sigma(X)$ is the many-sorted term algebra generated by variables from $X$ and applications of symbols of $\Sigma$, a language $K$ is a family $K_s\subseteq T_\Sigma(X)_s$, and a congruence $\Phi$ is a family of equivalence relations $\Phi_s$ preserved by every basic operation. Here the assumption that $F$ is a finite-index congruence formation literally supplies, for every $X$, a nonempty set $F(X)$ of such congruences; closure of $F(X)$ under intersection; upward closure under inclusion of the componentwise relations; closure under pullback along every homomorphism $f:T_\Sigma(X)\to T_\Sigma(Y)$ for which, at every sort $s$, the map $x\mapsto[f_s(x)]_{\Theta_s}$ onto $T_\Sigma(Y)_s/{\Theta_s}$ is surjective; and, for each selected $\Phi$, finiteness of the disjoint union $\sum_{s\in S}T_\Sigma(X)_s/{\Phi_s}$. The asserted witness $\mathcal L$ must itself carry all the structure required of a regular-language formation: every $K\in\mathcal L(X)$ has finite-index syntactic congruence, where $x\equiv_K y$ means that every congruence $\Psi$ containing every congruence that saturates $K$ relates $x$ and $y$; every language saturated by the universal congruence belongs to $\mathcal L(X)$; whenever $K,M\in\mathcal L(X)$, every language saturated by the intersection of their syntactic congruences also belongs to $\mathcal L(X)$; and whenever $M\in\mathcal L(Y)$, $f:T_\Sigma(X)\to T_\Sigma(Y)$ is quotient-surjective at every sort with respect to the syntactic congruence of $M$, and $K$ is saturated by the pullback of that congruence along $f$, then $K\in\mathcal L(X)$. If a sort’s relevant carrier is empty, the corresponding elementwise conditions are vacuous; if $S=\varnothing$, all sort-indexed conditions are vacuous and every disjoint union used in the finite-index condition is empty and hence finite.