Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Universe.
Require Import HSet.
Require Import HIT.epi HIT.unique_choice.

Local Open Scope path_scope.

(** We prove that [epi + mono <-> IsEquiv] *)
Section iso.
  Context `{Univalence}.
  Variables X Y : HSet.
  Variable f : X -> Y.

  Lemma atmost1P_isinj (injf : isinj f)
  : forall y : Y, atmost1P (fun x => f x = y).
H: Univalence
X, Y: HSet
f: X -> Y
injf: isinj f
forall y : Y, atmost1P (fun x : X => f x = y)
  Proof.
H: Univalence
X, Y: HSet
f: X -> Y
injf: isinj f
forall y : Y, atmost1P (fun x : X => f x = y)
    unfold isinj, atmost1P in *.
H: Univalence
X, Y: HSet
f: X -> Y
injf: forall x0 x1 : X, f x0 = f x1 -> x0 = x1
forall (y : Y) (x1 x2 : X),
f x1 = y -> f x2 = y -> x1 = x2
    intros.
H: Univalence
X, Y: HSet
f: X -> Y
injf: forall x0 x1 : X, f x0 = f x1 -> x0 = x1
y: Y
x1, x2: X
X0: f x1 = y
X1: f x2 = y
x1 = x2
    apply injf.
H: Univalence
X, Y: HSet
f: X -> Y
injf: forall x0 x1 : X, f x0 = f x1 -> x0 = x1
y: Y
x1, x2: X
X0: f x1 = y
X1: f x2 = y
f x1 = f x2
    path_induction.
H: Univalence
X, Y: HSet
f: X -> Y
injf: forall x0 x1 : X, f x0 = f x1 -> x0 = x1
x1, x2: X
f x1 = f x1
    reflexivity.
  Defined.

  Definition isequiv_isepi_ismono (epif : isepi f) (monof : ismono f)
  : IsEquiv f.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
IsEquiv f
  Proof.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
IsEquiv f
    pose proof (@isepi_issurj _ _ _ f epif) as surjf.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
IsEquiv f
    pose proof (isinj_ismono _ monof) as injf.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
IsEquiv f
    pose proof (unique_choice
                  (fun y x => f x = y)
                  _
                  (fun y => (@center _ (surjf y), atmost1P_isinj injf y)))
      as H_unique_choice.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
IsEquiv f
    apply (isequiv_adjointify _ H_unique_choice.1).
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
(fun x : Y => f (H_unique_choice.1 x)) == idmap
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
(fun x : X => H_unique_choice.1 (f x)) == idmap
    -
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
(fun x : Y => f (H_unique_choice.1 x)) == idmap intro.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
x: Y
f (H_unique_choice.1 x) = x
      apply H_unique_choice.2.
    -
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
(fun x : X => H_unique_choice.1 (f x)) == idmap intro.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
x: X
H_unique_choice.1 (f x) = x
      apply injf.
H: Univalence
X, Y: HSet
f: X -> Y
epif: isepi f
monof: ismono f
surjf: ReflectiveSubuniverse.IsConnMap
  (Modality.modality_to_reflective_subuniverse
     (Core.Tr (-1))) f
injf: isinj f
H_unique_choice: {f0 : Y -> X &
forall x : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
  (f0 x)}
x: X
f (H_unique_choice.1 (f x)) = f x
      apply H_unique_choice.2.
  Defined.
End iso.