The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Pierre-Marie Pedrot wrote:
> 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.

I think it's worth pointing out that this whole class of "Axiom of 
Choice"-style functions is much less interesting in Coq than in 
mainstream math.  An axiom like [realize] only becomes similarly 
interesting when you add other axioms of a classical flavor, like the 
law of the excluded middle.  This is because [inhabited A] still 
requires a constructive proof of the existence of a member of [A], which 
implies the existence of an algorithm for computing that member, so why 
bother using realize!  (The same holds true in versions that also 
require a proof that there exists (possibly a unique) element of [A] 
satisfying a predicate.)

With the law of the excluded middle, the [inhabited] proof effectively 
gains the ability to use a richer notion of computation.  Even without 
such an axiom, it already has a richer notion than in [Set], because 
[Prop] allows impredicativity, but my suspicion is that few proofs make 
deep use of impredicativity.  (Does anyone have a non-contrived 
counterexample to that suspicion?)