Skip to main content
1 of 2
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Au contaire. Like all questions of this kind it depends on the wording.

Let $S$ be an inhabited set of inhabited sets, so we are given $x_0\in X_0)\in S$.

If we are also given bijections $f_{X,Y}:X\cong Y$ for each pair $X,Y\in S$ then in particular we have $f_{X_0,Y}:X_0\cong Y$.

Therefore there is a defined element $y=f_{X_0,Y}(x_0)\in Y$ for each $Y\in S$.

No Choice required if the question is understood in this way.

Indeed, by substituting "inhabited" for "non-empty", Excluded Middle is also avoided.

Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58