(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Sigma.
Local Open Scope path_scope.


(** * Null homotopies of maps *)
Section NullHomotopy.
  Context `{Funext}.

  (** Geometrically, a nullhomotopy of a map [f : X -> Y] is an extension of [f] to a map [Cone X -> Y].  One might more simply call it e.g. [Constant f], but that is a little ambiguous: it could also reasonably mean e.g. a factorisation of [f] through [ Trunc -1 X ].  (Should the unique map [0 -> Y] be constant in one way, or in [Y]-many ways?) *)

  Definition NullHomotopy {X Y : Type} (f : X -> Y)
    := {y : Y & forall x:X, f x = y}.

  Lemma istrunc_nullhomotopy {n : trunc_index}
    {X Y : Type} (f : X -> Y) `{IsTrunc n Y}
    : IsTrunc n (NullHomotopy f).
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
IsTrunc n (NullHomotopy f)
  Proof.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
IsTrunc n (NullHomotopy f)
    apply @istrunc_sigma; auto.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
forall a : Y, IsTrunc n (forall x : X, f x = a)
    intros y.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
y: Y
IsTrunc n (forall x : X, f x = y) apply (@istrunc_forall _).
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
y: Y
forall a : X, IsTrunc n (f a = y)
    intros x.
H: Funext
n: trunc_index
X, Y: Type
f: X -> Y
IsTrunc0: IsTrunc n Y
y: Y
x: X
IsTrunc n (f x = y) apply istrunc_paths'.
  Defined.

  Definition nullhomotopy_homotopic {X Y : Type} {f g : X -> Y} (p : f == g)
    : NullHomotopy f -> NullHomotopy g.
H: Funext
X, Y: Type
f, g: X -> Y
p: f == g
NullHomotopy f -> NullHomotopy g
  Proof.
H: Funext
X, Y: Type
f, g: X -> Y
p: f == g
NullHomotopy f -> NullHomotopy g
    intros [y e].
H: Funext
X, Y: Type
f, g: X -> Y
p: f == g
y: Y
e: forall x : X, f x = y
NullHomotopy g
    exists y.
H: Funext
X, Y: Type
f, g: X -> Y
p: f == g
y: Y
e: forall x : X, f x = y
forall x : X, g x = y
    intros x; exact ((p x)^ @ e x).
  Defined.

  Definition nullhomotopy_composeR {X Y Z : Type} (f : X -> Y) (g : Y -> Z)
    : NullHomotopy g -> NullHomotopy (g o f).
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
NullHomotopy g -> NullHomotopy (g o f)
  Proof.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
NullHomotopy g -> NullHomotopy (g o f)
    intros [z e].
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
z: Z
e: forall x : Y, g x = z
NullHomotopy (fun x : X => g (f x))
    exists z.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
z: Z
e: forall x : Y, g x = z
forall x : X, g (f x) = z
    intros x; exact (e (f x)).
  Defined.

  Definition nullhomotopy_composeL {X Y Z : Type} (f : X -> Y) (g : Y -> Z)
    : NullHomotopy f -> NullHomotopy (g o f).
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
NullHomotopy f -> NullHomotopy (g o f)
  Proof.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
NullHomotopy f -> NullHomotopy (g o f)
    intros [y e].
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
y: Y
e: forall x : X, f x = y
NullHomotopy (fun x : X => g (f x))
    exists (g y).
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
y: Y
e: forall x : X, f x = y
forall x : X, g (f x) = g y
    intros x; exact (ap g (e x)).
  Defined.

  Definition cancelL_nullhomotopy_equiv
             {X Y Z : Type} (f : X -> Y) (g : Y -> Z) `{IsEquiv _ _ g}
    : NullHomotopy (g o f) -> NullHomotopy f.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv g
NullHomotopy (g o f) -> NullHomotopy f
  Proof.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv g
NullHomotopy (g o f) -> NullHomotopy f
    intros [z e].
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv g
z: Z
e: forall x : X, g (f x) = z
NullHomotopy f
    exists (g^-1 z).
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv g
z: Z
e: forall x : X, g (f x) = z
forall x : X, f x = g^-1 z
    intros x; apply moveL_equiv_V, e.
  Defined.

  Definition cancelR_nullhomotopy_equiv
             {X Y Z : Type} (f : X -> Y) (g : Y -> Z) `{IsEquiv _ _ f}
    : NullHomotopy (g o f) -> NullHomotopy g.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
NullHomotopy (g o f) -> NullHomotopy g
  Proof.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
NullHomotopy (g o f) -> NullHomotopy g
    intros [z e].
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
NullHomotopy g
    exists z.
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
forall x : Y, g x = z
    intros y; transitivity (g (f (f^-1 y))).
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
y: Y
g y = g (f (f^-1 y))
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
y: Y
g (f (f^-1 y)) = z
    -
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
y: Y
g y = g (f (f^-1 y)) symmetry; apply ap, eisretr.
    -
H: Funext
X, Y, Z: Type
f: X -> Y
g: Y -> Z
H0: IsEquiv f
z: Z
e: forall x : X, g (f x) = z
y: Y
g (f (f^-1 y)) = z apply e.
  Defined.

  Definition nullhomotopy_ap {X Y : Type} (f : X -> Y) (x1 x2 : X)
    : NullHomotopy f -> NullHomotopy (@ap _ _ f x1 x2).
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
NullHomotopy f -> NullHomotopy (ap f)
  Proof.
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
NullHomotopy f -> NullHomotopy (ap f)
    intros [y e].
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
NullHomotopy (ap f)
    unshelve eexists.
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
f x1 = f x2
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
forall x : x1 = x2, ap f x = ?y
    -
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
f x1 = f x2 exact (e x1 @ (e x2)^).
    -
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
forall x : x1 = x2, ap f x = e x1 @ (e x2)^ intros p.
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
p: x1 = x2
ap f p = e x1 @ (e x2)^
      apply moveL_pV.
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
p: x1 = x2
ap f p @ e x2 = e x1
      refine (concat_Ap e p @ _).
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
p: x1 = x2
e x1 @ ap (fun _ : X => y) p = e x1
      refine (_ @ concat_p1 _); apply ap.
H: Funext
X, Y: Type
f: X -> Y
x1, x2: X
y: Y
e: forall x : X, f x = y
p: x1 = x2
ap (fun _ : X => y) p = 1
      apply ap_const.
  Defined.

End NullHomotopy.