ch:algebraic-subtyping: ch:algebraic-subtyping

The outer arrow reverses its domain, and the inner arrow reverses once more. Thus $\alpha$ in $\alpha \to \mathsf{Bool}$ is positive overall, while the final occurrence in $\mathsf{Unit}\to \alpha$ is positive. An upper-bound elimination changes negative occurrences only, so it changes neither of these two occurrences in this whole positive type.

For $P{\le }_{\mathsf{a}}\alpha$, map a constrained instance $T$, with $\rho (P){\le }_{\mathsf{a}}T$, to the same image. Join introduction gives $T{\le }_{\mathsf{a}}\rho (P)\vee T$, while the bound and reflexivity give $\rho (P)\vee T{\le }_{\mathsf{a}}T$ by join elimination. Thus the two types are equivalent by mutual subtyping, not literal syntax. Conversely, for an arbitrary eliminated instance with image $T$, instantiate the constrained scheme at $\rho (P)\vee T$. This image satisfies the lower bound. Positive occurrences agree with the eliminated instance, while $T{\le }_{\mathsf{a}}\rho (P)\vee T$ compares the negative occurrences in the required direction. Structural induction on the polar scheme, reversing the comparison in arrow domains, proves equality of the two upward-closed instance sets.

If the two branch variables have output types $\alpha ,\beta$, the body has $\alpha \vee \beta$. A polar scheme is $\mathsf{Bool}\to {\alpha }^{-}\to {\beta }^{-}\to ({\alpha }^{+}\vee {\beta }^{+})$. Instantiating both variables with $\mathsf{Int}$ gives the ordinary type ending in $\mathsf{Int}$; instantiating both with $\mathsf{Bool}$ gives the one ending in $\mathsf{Bool}$. Neither ordinary arrow type is an instance of the other when the ground types are incomparable.

Polar bisubstitution and principal polar schemes belong only to MLsub. Boolean complement and characteristic Boolean homomorphisms belong only to ${\mathsf{BAS}}_0$. Guarded equi-recursion belongs to both, but in MLsub it supports polar automata and biunification, whereas in ${\mathsf{BAS}}_0$ the contractiveness condition supports the tagged-value Boolean semantics.

Arrow decomposition yields $\mathsf{Int}\vee \mathsf{Bool}{\le }_{\mathsf{a}}\alpha$ and $\beta {\le }_{\mathsf{a}}\mathsf{String}\wedge \gamma$. Lower elimination gives ${\alpha }^{+}=(\mathsf{Int}\vee \mathsf{Bool})\vee \alpha$ and ${\alpha }^{-}=\alpha$. Upper elimination gives ${\beta }^{-}=(\mathsf{String}\wedge \gamma )\wedge \beta$ and ${\beta }^{+}=\beta$. The untouched faces record exactly the direction of flow.

Assign $\alpha =\mathrm{\top }$ and $\beta =\mathrm{\perp }$. Both directed constraints hold, but equality would require $\mathrm{\top }=\mathsf{Int}\vee \mathsf{Bool}$ and $\mathrm{\perp }=\mathsf{String}\wedge \gamma$. Equality’s solution obtained by making those identifications is recovered by instantiating the free polar faces of the biunification result at the same types.

A scheme translation must also map the negative environment ${\mathrm{\Delta }}^{-}$ and prove that source instantiation corresponds to target substitution; the proposed equations specify neither. The Boolean equation $T\vee \mathrm{\neg }T=1$ is formed in ${\mathsf{BAS}}_0$. Its source counterpart is not formed because MLsub has no complement constructor. Hence the proposed map cannot transport the MLsub principality theorem.