Corollary. Derived products of retraction pairs [dt-0057]

It follows from the definition of retraction pairs that, for a pair $\xtofrom [g]{f}$ :

$f$ and $g$ are strict, i.e. $f(\bot ) = \bot$ and $g(\bot ) = \bot$ .
$g$ is uniquely determined by $f$ and vice-versa, so if another retraction pair $\xtofrom [g']{f}$ exists, then $g = g'$ . To see why, remember that $f$ and $g$ must be continuous and therefore monotonic.
$A$ is isomorphic to the range of $f$ , i.e. $A \simeq \{ f(x) \mid x \in A\} \subseteq B$ .

Problem. Contravariance in the function arrow [dt-0053]


( $y \mapsto b \mapsto z$ but $z \not \sqsubseteq y$ )	( $b \mapsto x \mapsto a$ but $a \neq b$ )