From Coq Require Import ClassicalDescription Ensembles Image
  ProofIrrelevance.
Import ProofIrrelevanceFacts.
From ZornsLemma Require Import EnsemblesImplicit FunctionProperties ImageImplicit.
From hydras Require Import MoreEpsilonIota.

Set Implicit Arguments.

Section AB_given.
  Variables (A B : Type)
            (Ha : inhabited A)
            (Hb:inhabited B)
            (DA: Ensemble A)
            (DB : Ensemble B).

Definition iota_fun (R:A→B→ Prop) : A → B :=
  fun a ⇒ iota Hb (fun b':B ⇒ In DA a ∧ R a b' ∧ In DB b').

Lemma iota_fun_e (R:A→B→ Prop):
  ∀ (a:A), In DA a →
   (∃ ! b, R a b ∧ In DB b) →
   unique (fun b ⇒ (R a b ∧ In DB b)) (iota_fun R a).

Lemma iota_fun_ind (P:A → Prop)
      (Q R:A→B→ Prop):
  ∀ (a x:A), In DA a → a = x →
   (∃ ! b, R a b ∧ In DB b) →
   P a →
   (∀ b, unique (fun b ⇒ R a b ∧ In DB b) b → Q a b) →
   Q x (iota_fun R a).

Section f_given.

  Variable f : A → B.

  Variable Rf : A → B → Prop.

  Definition rel_domain := ∀ a, In DA a → ∃ b, Rf a b .
  Definition rel_codomain := ∀ a b, In DA a → Rf a b → In DB b.
  Definition rel_functional := ∀ a b b', In DA a →
                              Rf a b → Rf a b' → b = b'.
  Definition rel_onto := ∀ b, In DB b → ∃ a, In DA a ∧ Rf a b.
  Definition rel_inj := ∀ a a' b, In DA a →
                                       In DA a' →
                                       Rf a b →
                                       Rf a' b →
                                       a = a'.

  Inductive rel_injection : Prop :=
   rel_inj_i : rel_domain → rel_codomain →
        rel_functional →
        rel_inj →
        rel_injection.

  Inductive rel_bijection : Prop :=
   rel_bij_i : rel_domain → rel_codomain →
        rel_functional →
        rel_onto →
        rel_inj →
        rel_bijection.

  Definition fun_codomain := ∀ a, In DA a → In DB (f a).
  Definition fun_onto := ∀ b, In DB b → ∃ a, In DA a ∧ f a = b.
  Definition fun_inj := ∀ a a' , In DA a → In DA a' → f a = f a' →
                 a = a'.

  Definition image := fun b ⇒ ∃ a, In DA a ∧ f a = b.

  Inductive fun_injection : Prop :=
   fun_inj_i : fun_codomain →
                            fun_inj → fun_injection.

  Inductive fun_bijection : Prop :=
   fun_bij_i : fun_codomain → fun_onto →
                            fun_inj → fun_bijection.

  Definition rel_inv := fun b a ⇒ In DA a ∧ In DB b ∧ Rf a b.

End f_given.

 Section rel_to_fun.

 Variables
           (Rf : A → B → Prop).

 Definition r2i := iota_fun Rf.

End rel_to_fun.
End AB_given.

Section inversion_of_bijection.
  Variables (A B : Type)
           (inhA : inhabited A)
           (DA : Ensemble A)
           (DB : Ensemble B)
           (f : A → B).

 Let inv_spec := fun y x ⇒ In DA x ∧ In DB y ∧ f x = y.

 Definition inv_fun := r2i inhA DB DA inv_spec.

 Hypothesis f_b : fun_bijection DA DB f.

Lemma inv_compose :
  ∀ x, DA x → inv_fun (f x) = x.

Lemma inv_composeR : ∀ b, DB b → f (inv_fun b) = b.

Lemma inv_fun_bij : fun_bijection DB DA inv_fun.

End inversion_of_bijection.

Lemma image_as_Im {A B : Type} (U : Ensemble A) (f : A → B) :
  image U f = Im U f.

Definition fun_restr {U V : Type} (f : U → V)
  {A : Ensemble U} {B : Ensemble V}
  (Hf : fun_codomain A B f) :
  { x : U | In A x } → { y : V | In B y } :=
  fun p : { x : U | In A x } ⇒
    exist (fun y : V ⇒ In B y)
      (f (proj1_sig p))
      (Hf (proj1_sig p) (proj2_sig p)).

Lemma fun_bijection_codomain
  {U V : Type} {A : Ensemble U} {B : Ensemble V}
  (g : U → V) (g_bij : fun_bijection A B g) :
  fun_codomain A B g.

Lemma fun_bijection_is_ZL_bijection
  {U V : Type} {A : Ensemble U} {B : Ensemble V}
  (g : U → V) (g_bij : fun_bijection A B g) :
  FunctionProperties.bijective
    (fun_restr (fun_bijection_codomain g_bij)).