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

Local Open Scope path_scope.
Local Open Scope trunc_scope.

(** * Varieties of constant function *)

(** Recall that a function [f : X -> Y] is *weakly constant*, [WeaklyConstant f], if [forall x y, f x = f y].  We show, following Kraus, Escardó, Coquand, and Altenkirch, that the type of fixed points of a weakly constant endofunction is an hprop.  However, to avoid potential confusion with [Coq.Init.Wf.Fix], instead of their notation [Fix], we denote this type by [FixedBy]. *)

Definition FixedBy {X : Type} (f : X -> X) := {x : X & f x = x}.

Instance ishprop_fix_wconst {X : Type} (f : X -> X)
  {wc : WeaklyConstant f}
  : IsHProp (FixedBy f).
X: Type
f: X -> X
wc: WeaklyConstant f
IsHProp (FixedBy f)
Proof.
X: Type
f: X -> X
wc: WeaklyConstant f
IsHProp (FixedBy f)
  apply hprop_inhabited_contr; intros [x0 p0].
X: Type
f: X -> X
wc: WeaklyConstant f
x0: X
p0: f x0 = x0
Contr (FixedBy f)
  refine (contr_equiv' {x:X & f x0 = x} _); unfold FixedBy.
X: Type
f: X -> X
wc: WeaklyConstant f
x0: X
p0: f x0 = x0
{x : X & f x0 = x} <~> {x : X & f x = x}
  apply equiv_functor_sigma_id.
X: Type
f: X -> X
wc: WeaklyConstant f
x0: X
p0: f x0 = x0
forall a : X, f x0 = a <~> f a = a intros x.
X: Type
f: X -> X
wc: WeaklyConstant f
x0: X
p0: f x0 = x0
x: X
f x0 = x <~> f x = x
  apply equiv_concat_l.
X: Type
f: X -> X
wc: WeaklyConstant f
x0: X
p0: f x0 = x0
x: X
f x = f x0
  apply wconst.
Defined.

(** It follows that if a type [X] admits a weakly constant endofunction [f], then [FixedBy f] is equivalent to [merely X]. *)
Definition equiv_fix_merely {X : Type} (f : X -> X)
  {wc : WeaklyConstant f}
  : FixedBy f <~> merely X.
X: Type
f: X -> X
wc: WeaklyConstant f
FixedBy f <~> merely X
Proof.
X: Type
f: X -> X
wc: WeaklyConstant f
FixedBy f <~> merely X
  apply equiv_iff_hprop.
X: Type
f: X -> X
wc: WeaklyConstant f
FixedBy f -> merely X
X: Type
f: X -> X
wc: WeaklyConstant f
merely X -> FixedBy f
  -
X: Type
f: X -> X
wc: WeaklyConstant f
FixedBy f -> merely X intros [x p]; exact (tr x).
  -
X: Type
f: X -> X
wc: WeaklyConstant f
merely X -> FixedBy f apply Trunc_rec; intros x.
X: Type
f: X -> X
wc: WeaklyConstant f
x: X
FixedBy f
    exists (f x).
X: Type
f: X -> X
wc: WeaklyConstant f
x: X
f (f x) = f x
    apply wconst.
Defined.

(** Therefore, a type is collapsible (admits a weakly constant endomap) if and only if [merely X -> X] (it has "split support"). *)
Definition splitsupp_collapsible {X} `{Collapsible X}
  : merely X -> X.
X: Type
H: Collapsible X
merely X -> X
Proof.
X: Type
H: Collapsible X
merely X -> X
  refine (_ o (equiv_fix_merely collapse)^-1).
X: Type
H: Collapsible X
FixedBy collapse -> X
  exact pr1.
Defined.

Definition collapsible_splitsupp {X} (s : merely X -> X)
  : Collapsible X.
X: Type
s: merely X -> X
Collapsible X
Proof.
X: Type
s: merely X -> X
Collapsible X
  refine (Build_Collapsible _ (s o tr) _); intros x y.
X: Type
s: merely X -> X
x, y: X
s (tr x) = s (tr y)
  apply (ap s), path_ishprop.
Defined.

(**  We say that [f] is *conditionally constant* if it factors through the propositional truncation [merely X], and *constant* if it factors through [Unit]. *)

Definition ConditionallyConstant {X Y : Type} (f : X -> Y)
  := ExtensionAlong (@tr (-1) X) (fun _ => Y) f.

(** We don't yet have a need for a predicate [Constant] on functions; we do already have the operation [const] which constructs the constant function at a given point.  Every such constant function is, of course, conditionally constant. *)
Definition cconst_const {X Y} (y : Y)
  : ConditionallyConstant (@const X Y y).
X, Y: Type
y: Y
ConditionallyConstant (const y)
Proof.
X, Y: Type
y: Y
ConditionallyConstant (const y)
  exists (const y); intros x; reflexivity.
Defined.

(** The type of conditionally constant functions is equivalent to [merely X -> Y]. *)
Definition equiv_cconst_from_merely `{Funext} (X Y : Type)
  : { f : X -> Y & ConditionallyConstant f } <~> (merely X -> Y).
H: Funext
X, Y: Type
{f : X -> Y & ConditionallyConstant f} <~>
(merely X -> Y)
Proof.
H: Funext
X, Y: Type
{f : X -> Y & ConditionallyConstant f} <~>
(merely X -> Y)
  refine (_ oE (equiv_sigma_symm _)).
H: Funext
X, Y: Type
{b : Trunc (-1) X -> Y &
{a : X -> Y & forall x : X, b (tr x) = a x}} <~>
(merely X -> Y)
  exact (equiv_sigma_contr _).
Defined.

(** If a function factors through any hprop, it is conditionally constant. *)
Definition cconst_factors_hprop {X Y : Type} (f : X -> Y)
  (P : Type) `{IsHProp P}
  (g : X -> P) (h : P -> Y) (p : h o g == f)
  : ConditionallyConstant f.
X, Y: Type
f: X -> Y
P: Type
IsHProp0: IsHProp P
g: X -> P
h: P -> Y
p: h o g == f
ConditionallyConstant f
Proof.
X, Y: Type
f: X -> Y
P: Type
IsHProp0: IsHProp P
g: X -> P
h: P -> Y
p: h o g == f
ConditionallyConstant f
  pose (g' := Trunc_rec g : merely X -> P).
X, Y: Type
f: X -> Y
P: Type
IsHProp0: IsHProp P
g: X -> P
h: P -> Y
p: h o g == f
g':= Trunc_rec g : merely X -> P: merely X -> P
ConditionallyConstant f
  exists (h o g'); intros x.
X, Y: Type
f: X -> Y
P: Type
IsHProp0: IsHProp P
g: X -> P
h: P -> Y
p: h o g == f
g':= Trunc_rec g : merely X -> P: merely X -> P
x: X
h (g' (tr x)) = f x
  apply p.
Defined.

(** Thus, if it factors through a type that [X] implies is contractible, then it is also conditionally constant. *)
Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
  (P : Type) {Pc : X -> Contr P}
  (g : X -> P) (h : P -> Y) (p : h o g == f)
  : ConditionallyConstant f.
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
ConditionallyConstant f
Proof.
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
ConditionallyConstant f
  assert (merely X -> IsHProp P).
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
merely X -> IsHProp P
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
X0: merely X -> IsHProp P
ConditionallyConstant f
  {
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
merely X -> IsHProp P apply Trunc_rec.            (** Uses funext *)
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
X -> IsHProp P
    intros x; pose (Pc x); exact istrunc_succ. }
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
X0: merely X -> IsHProp P
ConditionallyConstant f
  pose (g' := Trunc_ind (fun _ => P) g : merely X -> P).
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
X0: merely X -> IsHProp P
g':= Trunc_ind (fun _ : Trunc (-1) X => P) g
:
merely X -> P: merely X -> P
ConditionallyConstant f
  exists (h o g'); intros x.
H: Funext
X, Y: Type
f: X -> Y
P: Type
Pc: X -> Contr P
g: X -> P
h: P -> Y
p: h o g == f
X0: merely X -> IsHProp P
g':= Trunc_ind (fun _ : Trunc (-1) X => P) g
:
merely X -> P: merely X -> P
x: X
h (g' (tr x)) = f x
  apply p.
Defined.

(** Any weakly constant function with collapsible domain is conditionally constant. *)
Definition cconst_wconst_collapsible {X Y : Type} `{Collapsible X}
  (f : X -> Y) {wc : WeaklyConstant f}
  : ConditionallyConstant f.
X, Y: Type
H: Collapsible X
f: X -> Y
wc: WeaklyConstant f
ConditionallyConstant f
Proof.
X, Y: Type
H: Collapsible X
f: X -> Y
wc: WeaklyConstant f
ConditionallyConstant f
  exists (f o splitsupp_collapsible); intros x.
X, Y: Type
H: Collapsible X
f: X -> Y
wc: WeaklyConstant f
x: X
f (splitsupp_collapsible (tr x)) = f x
  unfold splitsupp_collapsible; simpl.
X, Y: Type
H: Collapsible X
f: X -> Y
wc: WeaklyConstant f
x: X
f (collapse x) = f x
  apply wconst.
Defined.

(** The image of a weakly constant function with hset codomain is an hprop. In fact, we just need to assume that [merely X -> IsHSet Y]. *)
Local Instance hprop_image_wconst_hset_if_merely_domain {X Y : Type} (f : X -> Y)
  {Ys : merely X -> IsHSet Y} {wc: WeaklyConstant f}
  : IsHProp (image (-1) f).
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
IsHProp (image (Tr (-1)) f)
Proof.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
IsHProp (image (Tr (-1)) f)
  apply hprop_allpath.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
forall x y : image (Tr (-1)) f, x = y
  intros [b m] [b' m'].
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
(b; m) = (b'; m')
  apply path_sigma_hprop; cbn.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
b = b'
  assert (Ys' : IsHSet Y).
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
IsHSet Y
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
Ys': IsHSet Y
b = b'
  {
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
IsHSet Y apply Ys.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
merely X strip_truncations.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b, b': Y
m': hfiber f b'
m: hfiber f b
merely X exact (tr m.1). }
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b: Y
m: Tr (-1) (hfiber f b)
b': Y
m': Tr (-1) (hfiber f b')
Ys': IsHSet Y
b = b'
  strip_truncations.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b, b': Y
Ys': IsHSet Y
m': hfiber f b'
m: hfiber f b
b = b'
  destruct m as [x p], m' as [x' p'].
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
b, b': Y
Ys': IsHSet Y
x': X
p': f x' = b'
x: X
p: f x = b
b = b'
  exact (p^ @ wc x x' @ p').
Defined.

(** When [merely X -> IsHSet Y], any weakly constant function [X -> Y] is conditionally constant. *)
Definition cconst_wconst_hset_if_merely_domain {X Y : Type} (f : X -> Y)
  {Ys : merely X -> IsHSet Y} {wc: WeaklyConstant f}
  : ConditionallyConstant f.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
ConditionallyConstant f
Proof.
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
ConditionallyConstant f
  srapply (cconst_factors_hprop f (image (-1) f)).
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
X -> image (Tr (-1)) f
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
image (Tr (-1)) f -> Y
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
?h o ?g == f
  -
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
X -> image (Tr (-1)) f apply factor1.
  -
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
image (Tr (-1)) f -> Y apply factor2.
  -
X, Y: Type
f: X -> Y
Ys: merely X -> IsHSet Y
wc: WeaklyConstant f
factor2 (image (Tr (-1)) f)
o factor1 (image (Tr (-1)) f) == f apply fact_factors.
Defined.

(** The previous result will be most often used when we know [Y] is an hset, so we specialize to this case. *)
Definition cconst_wconst_hset {X Y : Type} (f : X -> Y)
  {Ys : IsHSet Y} {wc : WeaklyConstant f}
  : ConditionallyConstant f
  := cconst_wconst_hset_if_merely_domain f (Ys:=fun _ => Ys).

(** We can decompose this into an "induction principle" and its computation rule. *)
Definition merely_rec_hset {X Y : Type} (f : X -> Y)
  {Ys : IsHSet Y} {wc : WeaklyConstant f}
  : merely X -> Y
  := (cconst_wconst_hset f).1.

(** The computation rule is [(cconst_wconst_hset f).2 x], but that's reflexivity. *)
Definition merely_rec_hset_beta {X Y : Type} (f : X -> Y)
  {Ys : IsHSet Y} {wc : WeaklyConstant f}
  (x : X)
  : merely_rec_hset f (tr x) = f x
  := idpath.

(** If we assume [Funext], then we can weaken the hypothesis from [merely X -> IsHSet Y] to [X -> IsHSet Y], since with [Funext], we know that [IsHSet Y] is an hprop. *)
Definition cconst_wconst_hset_if_domain `{Funext} {X Y : Type} (f : X -> Y)
  {Ys : X -> IsHSet Y} {wc : WeaklyConstant f}
  : ConditionallyConstant f
  := cconst_wconst_hset_if_merely_domain f (Ys:=Trunc_rec Ys).

(** We record the corresponding induction principle, but not the computation principle, since it is again definitional. *)
Definition merely_rec_hset_if_domain `{Funext} {X Y : Type} (f : X -> Y)
  {Ys : X -> IsHSet Y} {wc : WeaklyConstant f}
  : merely X -> Y
  := (cconst_wconst_hset_if_domain f).1.

(** The type of weakly constant functions [X -> Y], when [Y] is a set, is equivalent to [merely X -> Y]. This uses [Funext] for the main argument, so we may as well state it with the more general assumption [X -> IsHSet Y]. *)
Definition equiv_merely_rec_hset_if_domain `{Funext} (X Y : Type)
  {Ys : X -> IsHSet Y}
  : { f : X -> Y & WeaklyConstant f } <~> (merely X -> Y).
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
Proof.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
  pose proof (Ys' := Trunc_rec Ys : merely X -> IsHSet Y).
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} <~> (merely X -> Y)
  snapply equiv_adjointify.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} -> merely X -> Y
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
(merely X -> Y) -> {f : X -> Y & WeaklyConstant f}
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
?f o ?g == idmap
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
?g o ?f == idmap
  -
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
{f : X -> Y & WeaklyConstant f} -> merely X -> Y intros [f wc].
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
merely X -> Y  exact (merely_rec_hset_if_domain f (wc:=wc)).
  -
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
(merely X -> Y) -> {f : X -> Y & WeaklyConstant f} intro g.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
g: merely X -> Y
{f : X -> Y & WeaklyConstant f}  exists (g o tr).
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
g: merely X -> Y
WeaklyConstant (fun x : X => g (tr x))
    intros x y; apply (ap g), path_ishprop.
  -
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
(fun X0 : {f : X -> Y & WeaklyConstant f} =>
 (fun (f : X -> Y) (wc : WeaklyConstant f) =>
  merely_rec_hset_if_domain f) X0.1 X0.2)
o (fun g : merely X -> Y =>
   (fun x : X => g (tr x);
   (fun x y : X => ap g (path_ishprop (tr x) (tr y)))
   :
   WeaklyConstant (fun x : X => g (tr x)))) == idmap intros g; apply path_arrow; intros mx.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
g: merely X -> Y
mx: merely X
merely_rec_hset_if_domain (fun x : X => g (tr x)) mx =
g mx
    pose proof (Ys' mx).
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
g: merely X -> Y
mx: merely X
X0: IsHSet Y
merely_rec_hset_if_domain (fun x : X => g (tr x)) mx =
g mx
    strip_truncations; reflexivity.
  -
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
(fun g : merely X -> Y =>
 (fun x : X => g (tr x);
 (fun x y : X => ap g (path_ishprop (tr x) (tr y)))
 :
 WeaklyConstant (fun x : X => g (tr x))))
o (fun X0 : {f : X -> Y & WeaklyConstant f} =>
   (fun (f : X -> Y) (wc : WeaklyConstant f) =>
    merely_rec_hset_if_domain f) X0.1 X0.2) == idmap intros [f wc].
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
(fun x : X => merely_rec_hset_if_domain f (tr x);
fun x y : X =>
ap (merely_rec_hset_if_domain f)
  (path_ishprop (tr x) (tr y))) = (f; wc)
    snapply path_sigma; cbn.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
(fun x : X => f x) = f
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
transport (fun f : X -> Y => WeaklyConstant f) ?Goal
  (fun x y : X =>
   ap
     (fun x0 : Trunc (-1) X =>
      (Trunc_rec (fun a : X => (f a; tr (a; 1))) x0).1)
     (path_ishprop (tr x) (tr y))) = wc
    +
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
(fun x : X => f x) = f reflexivity.
    +
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
transport (fun f : X -> Y => WeaklyConstant f) 1
  (fun x y : X =>
   ap
     (fun x0 : Trunc (-1) X =>
      (Trunc_rec (fun a : X => (f a; tr (a; 1))) x0).1)
     (path_ishprop (tr x) (tr y))) = wc cbn.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
(fun x y : X =>
 ap
   (fun x0 : Trunc (-1) X =>
    (Trunc_rec (fun a : X => (f a; tr (a; 1))) x0).1)
   (path_ishprop (tr x) (tr y))) = wc funext x y.
H: Funext
X, Y: Type
Ys: X -> IsHSet Y
Ys': merely X -> IsHSet Y
f: X -> Y
wc: WeaklyConstant f
x, y: X
ap
  (fun x : Trunc (-1) X =>
   (Trunc_rec (fun a : X => (f a; tr (a; 1))) x).1)
  (path_ishprop (tr x) (tr y)) = wc x y
      pose (Ys x); apply path_ishprop.
Defined.

(** We can use the above to give a funext-free approach to defining a map by factoring through a surjection. *)

Section SurjectiveFactor.
  Context {A B C : Type} `{IsHSet C} (f : A -> C) (g : A -> B)
    (resp : forall x y, g x = g y -> f x = f y).

  (** The assumption [resp] tells us that [f o pr1] is weakly constant on each fiber of [g], so it factors through the propositional truncation. *)
  Definition surjective_factor_aux (b : B) : merely (hfiber g b) -> C.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
b: B
merely (hfiber g b) -> C
  Proof.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
b: B
merely (hfiber g b) -> C
    rapply (merely_rec_hset (f o pr1)).
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
b: B
WeaklyConstant (fun x : {x : A & g x = b} => f x.1)
    intros [x p] [y q]; cbn.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
b: B
x: A
p: g x = b
y: A
q: g y = b
f x = f y
    exact (resp x y (p @ q^)).
  Defined.

  (** When [g] is surjective, those propositional truncations are contractible, giving us a way to get an element of [C]. *)
  Definition surjective_factor `{IsSurjection g} : B -> C.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
B -> C
  Proof.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
B -> C
    intro b.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
b: B
C
    exact (surjective_factor_aux b (center _)).
  Defined.

  Definition surjective_factor_factors `{IsSurjection g}
    : surjective_factor o g == f.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
surjective_factor o g == f
  Proof.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
surjective_factor o g == f
    intros a; unfold surjective_factor.
A, B, C: Type
IsHSet0: IsHSet C
f: A -> C
g: A -> B
resp: forall x y : A, g x = g y -> f x = f y
IsSurjection0: IsConnMap (Tr (-1)) g
a: A
surjective_factor_aux (g a)
  (center (merely (hfiber g (g a)))) = f a
    exact (ap (surjective_factor_aux (g a)) (contr (tr (a; idpath)))).
  Defined.

End SurjectiveFactor.