Library exercise

Require Import prelude.

Section CB.

  Variable EM : forall A : Type, A + ¬ A.

  Variable A B : Type.
  Variable f : A -> B.
  Variable g : B -> A.
  Variable f_inj : injective f.
  Variable g_inj : injective g.

  Inductive C : A -> Type :=
   C_i : forall b : B, (forall a, f a = b -> C a) -> C (g b).

  Definition g_inv (a : A) : C a -> B :=
    fun p => match p with
              C_i b _ => b
             end.

  Lemma g_g_inv_eq : forall a p, g (g_inv a p) = a.
   intros ? []; reflexivity.
  Qed.

  Lemma g_inv_g_eq : forall b p, g_inv (g b) p = b.
    intros; apply g_inj, g_g_inv_eq.
  Qed.

  Definition r : A -> B :=
    fun a => match EM (C a) with
              inl c => g_inv _ c
            | inr _ => f a
             end.

  Definition f_inv (b : B) : ¬ C (g b) -> A :=
    fun nc =>
    match EM (Σ a, f a = b) with
     inl p => π p
   | inr p => match nc (C_i b (curry (C := fun a _ => C a) (fun q => match p q return C (π q) with end))) with end
    end.

  Lemma f_f_inv_eq : forall b p, f (f_inv b p) = b.
    intros ? ?; unfold f_inv.
    destruct (EM (Σ a, f a = b)).
    - exact (π s).
    - exfalso; apply p; constructor; intros; exfalso; eauto.
  Qed.

  Lemma f_inv_f_eq : forall a p, f_inv (f a) p = a.
   intros; apply f_inj, f_f_inv_eq.
  Qed.

  Definition r_inv : B -> A :=
    fun b => match EM (C (g b)) with
              inl c => g b
            | inr c => f_inv _ c
             end.

  Lemma r_rinv : section_retraction r r_inv.
   intros a; unfold r.
   destruct (EM (C a)) as [c|nc]; unfold r_inv.
   + destruct (EM (C (g (g_inv a c)))).
     - apply g_g_inv_eq.
     - exfalso; rewrite g_g_inv_eq in *; auto.
   + destruct (EM (C (g (f a)))).
     - exfalso; apply nc. inversion c; subst.
       apply X, g_inj; auto.
     - apply f_inv_f_eq.
  Qed.

  Lemma rinv_r : section_retraction r_inv r.
   intros a; unfold r_inv, r.
   case_eq (EM (C (g a))); intros ? ?.
   + rewrite H; apply g_inv_g_eq.
   + destruct (EM (C (f_inv a f0))).
     - exfalso; apply f0; constructor; intros; subst.
       rewrite f_inv_f_eq in c; assumption.
     - apply f_f_inv_eq.
  Qed.

  Lemma inverse_r_r_inv : inverse r r_inv.
    split; [apply r_rinv | apply rinv_r].
  Qed.

  Lemma isomorphism_r : isomorphism r.
    exists r_inv; apply inverse_r_r_inv.
  Qed.

  Theorem CB : Σ r : A -> B, isomorphism r.
   exists r; apply isomorphism_r.
  Qed.

  Theorem explicit_CB : Σ r : A -> B, isomorphism r × (forall a, (r a = f a) + (g (r a) = a)).
    exists r; split; [apply isomorphism_r|].
    intros; unfold r; destruct (EM (C a)).
    + right; apply g_g_inv_eq.
    + left; reflexivity.
  Qed.

End CB.