gistfile1.txt

Require Import Utf8.
Require Import Setoid.
Require Import ChoiceFacts.

Definition ext := ∀ A B, ∀ R : A -> A -> Prop, ∀ T : A -> B -> Prop, Equivalence R ->
  (∀ x x' y, R x x' -> T x y -> T x' y) ->
  (∀ x, ∃ y, T x y) ->
  ∃ f : A -> B, ∀ x : A, T x (f x) /\ (∀ x' : A, R x x' -> f x = f x').

Definition alt := forall A (R : A -> A -> Prop),
    Equivalence R ->
    exists f : A -> A, (forall x, R x (f x)) /\ (forall x y, R x y -> f x = f y).

Lemma ext_to_alt : ext -> alt.
Proof.
  intros Ext A R HR.
  destruct (Ext A A R R HR) as [f Hf].
  - intros. transitivity x;auto.
    symmetry;auto.
  - intros x;exists x;reflexivity.
  - exists f;split.
    + intros x;apply Hf.
    + intros x;apply Hf.
Qed.

Lemma alt_to_ext : FunctionalChoice -> alt -> ext.
Proof.
  intros choose Alt A B R T HR H1 H2.
  apply choose in H2.
  destruct H2 as [f0 Hf0].
  pose proof (Alt _ _ HR) as [f1 [H3 H4]].
  exists (fun x => f0 (f1 x)).
  intros x;split.
  - apply H1 with (f1 x);auto.
    symmetry;auto.
  - intros x' Hx.
    f_equal. apply H4. trivial.
Qed.

Lemma ext_to_choice : ext -> FunctionalChoice.
Proof.
  intros Ext A B R HR.
  destruct (Ext A B eq R _) as [f Hf].
  - intros x x' y []. trivial.
  - trivial.
  - exists f. apply Hf.
Qed.