The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/01/2014 09:01 PM, Eddy Westbrook wrote:
> The nondep_AC axiom below is, I think, equivalent to the Type-Theoretic 
> Description Axiom (TTDA), which is this:
>
> Definition TTDA : Type :=
>    forall (A B : Type) (P : A -> B -> Prop),
>      (forall (a : A), exists b, P a b) ->
>      (exists f, forall (a : A), P a (f a)).

That looks like Coq.Logic.ClassicalChoice.choice.

> TTDA has some sort of non-constructive content, in that it, with 
> propositional Excluded Middle, allows you to prove informative Excluded 
> Middle. I am not what TTDA just by itself allows, however.
>
> -Eddy
>
> On Oct 1, 2014, at 5:29 AM, Pierre-Marie Pédrot 
> <pierre-marie.pedrot AT inria.fr>
>  wrote:
>
> > On 30/09/2014 22:47, Jonathan wrote:
> > > Anyone seen it before?
> > It seems instead equivalent to a weak form of a non-dependent axiom of
> > choice, rather than to excluded middle :
> >
> > Definition nondep_AC := forall A B, (A -> inhabited B) -> inhabited (A
> > -> B).
> > Definition escape := forall A, inhabited (inhabited A -> A).
> >
> > Lemma dir : nondep_AC -> escape.
> > Proof.
> > intros ac A; apply ac; trivial.
> > Qed.
> >
> > Lemma rev : escape -> nondep_AC.
> > Proof.
> > intros esc A B f.
> > destruct (esc B) as [g].
> > constructor; auto.
> > Qed.
> >
> > PMP