Require Import
        HoTT.Basics
        HoTT.Truncations.Core Modalities.Modality.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** Definition by factoring through a surjection. *)

Section surjective_factor.
  Context `{Funext}.
  Context {A B C} `{IsHSet C} `(f : A -> C) `(g : A -> B) {Esurj : IsSurjection g}.
  Variable (Eg : forall x y, g x = g y -> f x = f y).

  Lemma ishprop_surjective_factor_aux : forall b, IsHProp (exists c : C, forall a, g a = b -> f a = c).
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
forall b : B,
IsHProp {c : C & forall a : A, g a = b -> f a = c}
  Proof.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
forall b : B,
IsHProp {c : C & forall a : A, g a = b -> f a = c}
    intros.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
b: B
IsHProp {c : C & forall a : A, g a = b -> f a = c} apply Sigma.ishprop_sigma_disjoint.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
b: B
forall x y : C,
(forall a : A, g a = b -> f a = x) ->
(forall a : A, g a = b -> f a = y) -> x = y
    intros c1 c2 E1 E2.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
b: B
c1, c2: C
E1: forall a : A, g a = b -> f a = c1
E2: forall a : A, g a = b -> f a = c2
c1 = c2
    generalize (@center _ (Esurj b)); apply (Trunc_ind _).
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
b: B
c1, c2: C
E1: forall a : A, g a = b -> f a = c1
E2: forall a : A, g a = b -> f a = c2
hfiber g b -> c1 = c2
    intros [a p];destruct p.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
c1, c2: C
a: A
E1: forall a0 : A, g a0 = g a -> f a0 = c1
E2: forall a0 : A, g a0 = g a -> f a0 = c2
c1 = c2
    path_via (f a).
  Qed.

  Definition surjective_factor_aux :=
    @conn_map_elim
      _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c)
      ishprop_surjective_factor_aux
      (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)).

  Definition surjective_factor : B -> C
    := fun b => (surjective_factor_aux b).1.

  Lemma surjective_factor_pr : f == compose surjective_factor g.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
f == surjective_factor o g
  Proof.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
f == surjective_factor o g
    intros a.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
a: A
f a = surjective_factor (g a)
    apply (surjective_factor_aux (g a)).2.
H: Funext
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
Esurj: IsConnMap (Tr (-1)) g
Eg: forall x y : A, g x = g y -> f x = f y
a: A
g a = g a trivial.
  Qed.

End surjective_factor.