The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Yes, you are right, thanks!

I got the name TTDA from Werner's paper "Sets in Types, Types in Sets", where 
he has a different axiom that he calls a choice principle.

It also looks like AC_fun in Coq.Logic.ChoiceFacts.

So, then, does this version of choice imply excluded middle? I can't find a 
proof in the standard library...

Eddy

Sent from my iPhone

> On Oct 1, 2014, at 6:12 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
> 
>> 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
>