Congruence-formation recovery identity

For every type $S$ equipped with the proposition that $S$ is finite (no enumeration, decidable equality, or inhabitant is assumed), every $S$-sorted signature $\Sigma$ assigning a type of operation symbols $\Sigma_{w,s}$ to each finite list $w$ of input sorts and output sort $s$, every finite-index congruence formation $F$ for $\Sigma$, and every regular-language formation $\mathcal L$ for $\Sigma$, the following conditional assertion holds. Here an $S$-sorted set $X$ is an arbitrary family of types $(X_s)_{s\in S}$, $T_\Sigma(X)_s$ is the type of well-sorted $\Sigma$-terms of sort $s$ whose variables come from $X$, a language $K$ on $T_\Sigma(X)$ is an arbitrary family of subsets $K_s\subseteq T_\Sigma(X)_s$, and a congruence $\Phi$ is a family of equivalence relations $\sim_{\Phi,s}$ on these term types that is preserved by every basic operation; $\Phi\leq\Psi$ means $\sim_{\Phi,s}$ is contained in $\sim_{\Psi,s}$ at every sort, $\Phi\cap\Psi$ is the sortwise intersection, the pullback $f^*\Theta$ along a homomorphism $f:T_\Sigma(X)\to T_\Sigma(Y)$ relates $x,y$ exactly when $f_s(x)\sim_{\Theta,s}f_s(y)$, and $\Phi$ has finite index exactly when the dependent disjoint union $\sum_{s\in S}T_\Sigma(X)_s/{\sim_{\Phi,s}}$ is finite. A congruence $\Phi$ saturates $K$ exactly when $x\sim_{\Phi,s}y$ implies $x\in K_s\Longleftrightarrow y\in K_s$ for every $s,x,y$. The syntactic congruence $\operatorname{Syn}(K)$ used below is literally the congruence for which $x\sim_{\operatorname{Syn}(K),s}y$ means that, for every congruence $\Psi$, if every congruence $\Phi$ saturating $K$ satisfies $\Phi\leq\Psi$, then $x\sim_{\Psi,s}y$; a language is called regular when this congruence has finite index. The bundled assumptions on $F$ are that for every $X$, $F(X)$ is a nonempty set of congruences on $T_\Sigma(X)$, is closed under binary intersection, is upward closed under $\leq$, contains $f^*\Theta$ whenever $\Theta\in F(Y)$ and the map $x\mapsto[f_s(x)]_\Theta:T_\Sigma(X)_s\to T_\Sigma(Y)_s/{\sim_{\Theta,s}}$ is surjective for every sort $s$, and contains only finite-index congruences. The bundled assumptions on $\mathcal L$ are that each $K\in\mathcal L(X)$ is regular; every $K$ saturated by the universal congruence (which relates every pair of terms of the same sort) belongs to $\mathcal L(X)$; whenever $K_1,K_2\in\mathcal L(X)$, every language saturated by $\operatorname{Syn}(K_1)\cap\operatorname{Syn}(K_2)$ also belongs to $\mathcal L(X)$; and whenever $M\in\mathcal L(Y)$, $f:T_\Sigma(X)\to T_\Sigma(Y)$ has each map $x\mapsto[f_s(x)]_{\operatorname{Syn}(M)}$ surjective, and $K$ is saturated by $f^*\operatorname{Syn}(M)$, then $K\in\mathcal L(X)$. If, for every arbitrary $S$-sorted set $X$, the selected languages are exactly $\mathcal L(X)=\{K\mid\exists\Phi\in F(X),\ \Phi\text{ saturates }K\}$, then, for every such $X$, the selected congruences are exactly $F(X)=\{\Phi\mid \sum_{s\in S}T_\Sigma(X)_s/{\sim_{\Phi,s}}\text{ is finite and, for every language }K,\ \Phi\text{ saturates }K\Rightarrow K\in\mathcal L(X)\}$. The quantifiers include $S=\varnothing$, empty or infinite variable types $X_s$, empty term sorts, nullary operations, and signatures having empty or infinite types of operation symbols; thus sortwise universal, compatibility, saturation, and surjectivity conditions can be vacuous on absent sorts or elements, the finite-index condition is automatic when $S$ is empty, and for any $F,\mathcal L$ for which the displayed language equality premise does not hold, the conditional assertion imposes no conclusion.