A Universe of Sorts

Given two injections $f: S \to T$ , $g: T \to S$ , we want to create a bijection.
Suppose we have $S = T = N$ , and $f(n) = g(n) = n + 1$ .
If $f$ were surjective, we are done, for then $f$ is the bijection.
In this case, $f$ is not surjective, because $T-f(S) = {0}$ . So $0$ has no preimage under $f$ .
We will create a new function $f'$ by perturbing $f$ , such that it does map some element in $X$ to $0$ [which is currently missed ].
Start with $f' \equiv f$ . This means that $f'$ misses $0$ .
We can "force" a pre-image for $0$ . How? Consider $g(0) = 1$ , and set $f'(g(0)) \equiv 0$ , or $f'(1) \equiv 0$ .
Whoops, but we have now "lost" a preimage for $f(1) = 2$ , as now $2$ is not in the image of $f'$ .
Let's repeat the same process and fix it the same way. $f'(g(2)) \equiv 2$ , or $f'(3) \equiv 2$ .
Now we have lost a pre-image for $f(3)$ . Well, we just repeat the construction. For how long?
Well, this is where we invoke the glory of a fixpoint theorem!
See that we definitely need to reverse the arrows for $(T-f(S))$ . If we start with a set $Y \subseteq T$ that we will reverse the arrows to, we will then need to reverse the arrows for $Y \cup F(G(Y))$ .
Thus, the set that we need to fiddle in $f'$ is $Y \mapsto (T-f(S))\cup F(G(Y))$ .

§ Cantor Schroder Bernstein via Fixpoint