Understanding a proof of Diaconescu's theorem
Solution 1:
Why can't we just let $f(X)=0$ and $f(Y)=1$.
Because the function has to be extensional. If $X = Y$ then the quoted definition would not give a function.
The proof is using $P∨¬P⟺T$, isn't it?
Yes, because equality for natural numbers is decidable: given two natural numbers $n,m$, the constructive systems to which Diaconescu's theorems applies will prove "$n = m \lor m \not = n$".