# 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.

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.