Regular-language-formation recovery identity

For every finite type $S$, every $S$-sorted signature $\Sigma$ assigning a type of operation symbols $\Sigma(w,s)$ to each finite input-sort list $w$ and output sort $s$, every regular-language formation $\mathcal L$ over $\Sigma$, and every finite-index congruence formation $\mathcal F$ over $\Sigma$, assume that for every arbitrary $S$-sorted family of variable types $X=(X_s)_{s\in S}$, $\mathcal F(X)$ is exactly the set of congruences $\Phi$ on the free algebra $T_\Sigma(X)$ such that (i) the disjoint union $\coprod_{s\in S}T_\Sigma(X)_s/{\Phi_s}$ of their quotient classes is finite and (ii) every sorted language $K=(K_s\subseteq T_\Sigma(X)_s)_{s\in S}$ saturated by $\Phi$—meaning $\Phi_s(t,u)$ implies $t\in K_s\iff u\in K_s$—belongs to $\mathcal L(X)$. Here $T_\Sigma(X)$ consists sortwise of the terms generated from variables in $X$ by the operations of $\Sigma$; a congruence is a sortwise equivalence relation compatible with every operation; and $\Phi\leq\Psi$ means $\Phi_s(t,u)\Rightarrow\Psi_s(t,u)$ at every sort. The packaged assumptions on $\mathcal F$ further say that $\mathcal F(X)$ is nonempty for every $X$, is closed under componentwise intersection, is upward closed under $\leq$, contains only finite-index congruences, and is closed under pullback as follows: if $\Theta\in\mathcal F(Y)$ and $f:T_\Sigma(X)\to T_\Sigma(Y)$ is a homomorphism for which $t\mapsto[f_s(t)]_{\Theta_s}$ is surjective at every sort, then the congruence $t\sim u\iff\Theta_s(f_s(t),f_s(u))$ belongs to $\mathcal F(X)$. The packaged assumptions on $\mathcal L$ say that every member of $\mathcal L(X)$ is regular, meaning that its syntactic congruence has finite index; that every language saturated by the universal congruence belongs to $\mathcal L(X)$; that whenever $K,N\in\mathcal L(X)$, every language saturated by the intersection of their syntactic congruences also belongs to $\mathcal L(X)$; and that if $M\in\mathcal L(Y)$, $f:T_\Sigma(X)\to T_\Sigma(Y)$ is sortwise surjective after quotienting by the syntactic congruence of $M$, and $K$ is saturated by that congruence’s pullback along $f$, then $K\in\mathcal L(X)$. Literally, the syntactic congruence used here relates $t,u$ of sort $s$ exactly when, for every congruence $\Psi$, if every congruence $\Phi$ saturating the language is contained in $\Psi$, then $\Psi_s(t,u)$. Under the displayed equality $\mathcal F(X)=\{\Phi:\Phi\text{ has finite index and every }\Phi\text{-saturated language lies in }\mathcal L(X)\}$ for all $X$, the conclusion is that for every $X$, $\mathcal L(X)$ is exactly $\{K:\exists\,\Phi\in\mathcal F(X)\text{ such that }K\text{ is saturated by }\Phi\}$, with no uniqueness required of the witnessing $\Phi$. All quantifiers include $S=\varnothing$, empty variable components $X_s$, empty term carriers, and signatures with empty operation-symbol types; no $X_s$ is assumed finite or inhabited. Consequently, sortwise compatibility and saturation clauses are vacuous on empty term carriers, all sort-indexed clauses are vacuous when $S$ is empty, and a required quotient-surjectivity premise may be impossible when its source carrier is empty but its target quotient is inhabited.