Require Import HoTT.Basics.Require Import HoTT.Basics.
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 : IsInjective f)
  : forall y : Y, atmost1P (fun x => f x = y).
H: Univalence
X, Y: HSet
f: X -> Y
injf: IsInjective f
forall y : Y, atmost1P (fun x : X => f x = y)
  Proof.
H: Univalence
X, Y: HSet
f: X -> Y
injf: IsInjective f
forall y : Y, atmost1P (fun x : X => f x = y)
    intros y x x' p q.
H: Univalence
X, Y: HSet
f: X -> Y
injf: IsInjective f
y: Y
x, x': X
p: f x = y
q: f x' = y
x = x'
    apply (injective f).
H: Univalence
X, Y: HSet
f: X -> Y
injf: IsInjective f
y: Y
x, x': X
p: f x = y
q: f x' = y
f x = f x'
    exact (p @ q^).
  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: IsInjective 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: IsInjective 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: IsInjective 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: IsInjective 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: IsInjective 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: IsInjective f
H_unique_choice: {f0 : Y -> X & forall x0 : Y, (fun (y : Y) (x1 : X) => f x1 = y) x0 (f0 x0)}
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: IsInjective 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: IsInjective f
H_unique_choice: {f0 : Y -> X & forall x0 : Y, (fun (y : Y) (x1 : X) => f x1 = y) x0 (f0 x0)}
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: IsInjective f
H_unique_choice: {f0 : Y -> X & forall x0 : Y, (fun (y : Y) (x1 : X) => f x1 = y) x0 (f0 x0)}
x: X
f (H_unique_choice.1 (f x)) = f x
      apply H_unique_choice.2.
  Defined.
End iso.