The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

A variant of this principle (with hprop-truncation instead than Prop-truncation) is considered in a recent paper by Kraus, Escardo, Coquand & Altenkirch [ http://www.cs.bham.ac.uk/~mhe/papers/hj.pdf ]. It's quite a long technical read I'm afraid.

On 1 October 2014 14:29, 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