The Coq mailing list

[Pierre-Marie Pedrot <pierremarie.pedrot AT ens-lyon.fr>]

> Parameter realize : forall {A:Type}, (A->Prop)->A.
> Axiom realization : forall {A:Type} (P:A->Prop), (exists! x:A, P x)
> -> P (realize P).

> (* Note that "unique existence (exists!)" is assumed instead of "mere
> existence (exist).")

> What are expected dangers of assuming each?

This :

Lemma PHAIL : False.
Proof.
apply realize;intros [].
Qed.

(Choice operator is inconsistent in Type Theory; you must assume that  
A is inhabited in realize, as :

Parameter realize : forall (A : Type), inhabited A -> (A -> Prop) -> A.

See the standard library Epsilon* modules for more informations.

PMP