The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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

Attachment: signature.asc
Description: OpenPGP digital signature