The Coq mailing list

["Dominique Larchey-Wendling" <dominique.larchey-wendling AT loria.fr>]

I think it is called reification in Coq. And yes it is the axiom of unique 
choice... The relation does not contain enough information to compute the 
value. Unless P is decidable and the type is enumerable of course.

Envoyé avec AquaMail pour Android
http://www.aqua-mail.com


Le 11 septembre 2016 11:09:23 Daniel de Rauglaudre 
<daniel.de_rauglaudre AT inria.fr> a écrit :

> Hi all,
>
> Is the axiom of choice required if all sets have one only element ?
> If not, how to prove it ?
>
> Russel said that if all sets contain a pair of socks, we need the axiom
> of choice to select a sock in each pair but that if they are shoes,
> we don't need it, because the choice function can be : "take the left
> shoe".
>
> But for sets of one only element ?
>
> Namely, I want to prove :
>    (∀ x, ∃! y, P x y) → ∃ f, ∀ x, P x (f x)
>
> Is is possible, or do I need the fucking axiom of choice ?
>
> Thanks.
>
> --
> Daniel de Rauglaudre
> http://pauillac.inria.fr/~ddr/