The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Ah indeed, axiom of unique choice... thanks. It is because somebody
told me the choice was computable in that case but I could not prove
it. Normal, if it is false :-)

On Sun, Sep 11, 2016 at 11:22:25AM +0200, Dominique Larchey-Wendling wrote:
> 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/
> 

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/