Library Coqtail.Fresh.Inhabited.Choice_facts

Axiom choice : ∀ A (B : A → Type), (∀ x, inhabited (B x)) → inhabited (∀ x, B x).

Definition epsilon := ∀ A (B : A → Prop), (∃ x, B x) → {x | B x}.

Definition T A := epsilon → A.
Definition U A := inhabited A.

Lemma U_T : ∀ A, T A → U A.
Proof.
intros A H; unfold T, U in ×.
assert (Hi : inhabited ((inhabited epsilon) → A)).
apply choice; auto.
intros [Hi]; constructor; intuition.
destruct Hi as [Hi]; constructor; apply Hi.
clear; unfold epsilon.
apply (choice Type); intros A; apply choice; intros B; apply choice.
intros [x Hx]; constructor; eauto.
Qed.

Lemma T_U : ∀ A, U A → T A.
Proof.
intros A H; unfold T, U in *; intros Heps.
destruct (Heps A (fun _ ⇒ True)); auto.
destruct H; eauto.
Qed.