A Universe of Sorts

Choice implies LEM
Let $P$ be a proposition. Build the sets $T, F$ as:
$T \equiv {x \in \{0, 1\} : (x = 1) \lor P}$ , and $F \equiv x \in \{ 0, 1 \} : (x = 0) \lor P \}$ .
Note that if we had LEM, we could case split on $P$ via LEM and show that $x \equiv \{ 1 \}$ if $P$ , and $x \equiv \{ 0, 1\}$ if $\not P$ .
However, we don't have LEM. So let's invoke Choice on the set $B \equiv \{T, F \}$ . This means we get a choice function $c: B \to \cup c B$ such that $c(T) \in T$ and $c(F) \in F$ .
By the definition of the two sets, this means that $(c(T) = 1 \lor P)$ , and $(c(F) = 0 \lor P)$ .
This can be written as the logical formula $(c(T) = 1 \lor P) \land (c(F) = 0 \lor P)$ .
This is the same as $(c(T) \neq c(F)) \lor P$ .
Now see that since $P \implies (U = V)$ (by extensionality), we have that $P \implies (f(U) = f(V))$ .
See that contraposition is available purely intuitionistically: ( (p -> q) -> (q -> false) -> p -> false).
Therefore, by contraposition $(f(U) \neq f(V)) \implies \lnot P$ .
This means we have $P \lor \lnot P$ !

§ Diaconescu's Theorem