Uniformization from determinacy (source code)

= Uniformization from determinacy

Under $\mathsf{AD}_{X}$, every relation $A\subseteq X\times X$ has a uniformization. Let the first moves of Players I and II be $x$ and $y$, and let II win when $x$ is outside the projection of $A$ or $(x,y)\in A$. Player I cannot have a winning strategy, so the first response of a winning strategy for II uniformizes $A$.