Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Basics.Equivalences.Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Basics.Equivalences.
Require Import Types.Unit Types.Paths Types.Universe Types.Sigma.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Colimits.Pushout Homotopy.Suspension.
Require Import Homotopy.NullHomotopy.
Require Import HFiber Limits.Pullback BlakersMassey.

Set Universe Minimization ToSet.

(** * Homotopy Cofibers *)

(** ** Definition *)

(** Homotopy cofibers or mapping cones are spaces constructed from a map [f : X -> Y] by contracting the image of [f] inside [Y] to a point. They can be thought of as a kind of coimage or quotient. *)

Definition Cofiber {X Y : Type} (f : X -> Y)
  := Pushout f (const_tt X).

(** *** Constructors *)

(** Any element of [Y] can be included in the cofiber. *)
Definition cofib {X Y : Type} (f : X -> Y) : Y -> Cofiber f
  := pushl.

(** We have a distinguished point in the cofiber, where the image of [f] is contracted to. *)
Definition cf_apex {X Y : Type} (f : X -> Y) : Cofiber f
  := pushr tt.

(** Given an element [x : X], we have the path [cfglue f x] from the [f x] to the [cf_apex]. *)
Definition cfglue {X Y : Type} (f : X -> Y) (x : X) : cofib f (f x) = cf_apex f
  := pglue _.

(** *** Induction and recursion principles *)

(** The recursion principle for the cofiber of [f : X -> Y] requires a function [g : Y -> Z] such that [g o f] is null homotopic, i.e. constant. *)
Definition cofiber_rec {X Y Z : Type} (f : X -> Y) (g : Y -> Z)
  (null : NullHomotopy (g o f))
  : Cofiber f -> Z.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Cofiber f -> Z
Proof.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Cofiber f -> Z
  snapply Pushout_rec.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Y -> Z
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Unit -> Z
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
forall a : X, ?pushb (f a) = ?pushc (const_tt X a)
  -
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Y -> Z exact g.
  -
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
Unit -> Z intros; exact null.1.
  -
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
forall a : X, g (f a) = unit_name null.1 (const_tt X a) intros a.
X, Y, Z: Type
f: X -> Y
g: Y -> Z
null: NullHomotopy (g o f)
a: X
g (f a) = unit_name null.1 (const_tt X a)
    exact (null.2 a).
Defined.

(** The induction principle is similar, although requires a dependent form of null homotopy. *)
Definition cofiber_ind {X Y : Type} (f : X -> Y) (P : Cofiber f -> Type)
  (g : forall y, P (cofib f y))
  (null : exists b, forall x, transport P (cfglue f x) (g (f x)) = b)
  : forall x, P x.
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall x : Cofiber f, P x
Proof.
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall x : Cofiber f, P x
  snapply Pushout_ind.
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall b : Y, P (pushl b)
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall c : Unit, P (pushr c)
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall a : X, transport P (pglue a) (?pushb (f a)) = ?pushc (const_tt X a)
  -
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall b : Y, P (pushl b) intros y; apply g.
  -
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall c : Unit, P (pushr c) intros []; exact null.1.
  -
X, Y: Type
f: X -> Y
P: Cofiber f -> Type
g: forall y : Y, P (cofib f y)
null: {b : P (cf_apex f) & forall x : X, transport P (cfglue f x) (g (f x)) = b}
forall a : X,
transport P (pglue a) ((fun y : Y => g y) (f a)) =
(fun c : Unit => match c as u return (P (pushr u)) with
                 | tt => null.1
                 end)
  (const_tt X a) exact null.2.
Defined.

(** ** Functoriality *)

Local Close Scope trunc_scope.

(** The homotopy cofiber can be thought of as a functor from the category of arrows in [Type] to [Type]. *)

(** 1-functorial action. *)
Definition functor_cofiber {X Y X' Y' : Type} {f : X -> Y} {f' : X' -> Y'}
  (g : X -> X') (h : Y -> Y') (p : h o f == f' o g)
  : Cofiber f -> Cofiber f'
  := functor_pushout g h idmap p (fun _ => idpath).

(** 2-functorial action. *)
Definition functor_cofiber_homotopy {X Y X' Y' : Type} {f : X -> Y} {f' : X' -> Y'}
  {g g' : X -> X'} {h h' : Y -> Y'} {p : h o f == f' o g} {p' : h' o f == f' o g'}
  (u : g == g') (v : h == h') 
  (r : forall x, p x @ ap f' (u x) = v (f x) @ p' x)
  : functor_cofiber g h p == functor_cofiber g' h' p'.
X, Y, X', Y': Type
f: X -> Y
f': X' -> Y'
g, g': X -> X'
h, h': Y -> Y'
p: h o f == f' o g
p': h' o f == f' o g'
u: g == g'
v: h == h'
r: forall x : X, p x @ ap f' (u x) = v (f x) @ p' x
functor_cofiber g h p == functor_cofiber g' h' p'
Proof.
X, Y, X', Y': Type
f: X -> Y
f': X' -> Y'
g, g': X -> X'
h, h': Y -> Y'
p: h o f == f' o g
p': h' o f == f' o g'
u: g == g'
v: h == h'
r: forall x : X, p x @ ap f' (u x) = v (f x) @ p' x
functor_cofiber g h p == functor_cofiber g' h' p'
  snapply (functor_pushout_homotopic u v (fun _ => 1) r).
X, Y, X', Y': Type
f: X -> Y
f': X' -> Y'
g, g': X -> X'
h, h': Y -> Y'
p: h o f == f' o g
p': h' o f == f' o g'
u: g == g'
v: h == h'
r: forall x : X, p x @ ap f' (u x) = v (f x) @ p' x
forall a : X,
(fun x : X => 1) a @ ap (const_tt X') (u a) =
(fun x : Unit => 1) (const_tt X a) @ (fun x : X => 1) a
  intro x; exact (concat_1p _ @ ap_const _ _).
Defined.

(** The cofiber functor preserves the identity map. *) 
Definition functor_cofiber_idmap {X Y : Type} (f : X -> Y)
  : functor_cofiber (f:=f) idmap idmap (fun _ => 1) == idmap
  := functor_pushout_idmap.

(** The cofiber functor preserves composition of squares. (When mapping parallel edges). *)
Definition functor_cofiber_compose {X Y X' Y' X'' Y'' : Type}
  {f : X -> Y} {f' : X' -> Y'} {f'' : X'' -> Y''}
  {g : X -> X'} {g' : X' -> X''} {h : Y -> Y'} {h' : Y' -> Y''}
  (p : h o f == f' o g) (p' : h' o f' == f'' o g')
  : functor_cofiber (g' o g) (h' o h) (fun x => ap h' (p x) @ p' (g x))
    == functor_cofiber g' h' p' o functor_cofiber g h p
  := functor_pushout_compose g h idmap g' h' idmap p (fun _ => 1) p' (fun _ => 1).

Local Open Scope trunc_scope.

(** ** Connectivity of cofibers *)

(** The cofiber of an [n]-connected map is [n.+1]-connected. *)
Definition isconnected_cofiber (n : trunc_index) {X Y : Type} (f : X -> Y)
  {fc : IsConnMap n f}
  : IsConnected n.+1 (Cofiber f).
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnected (Tr n.+1) (Cofiber f)
Proof.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnected (Tr n.+1) (Cofiber f)
  apply isconnected_from_elim.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
forall C : Type,
In (Tr n.+1) C -> forall f0 : Cofiber f -> C, NullHomotopy f0
  intros C H' g.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
NullHomotopy g
  exists (g (cf_apex _)).
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
forall x : Cofiber f, g x = g (cf_apex f)
  snapply cofiber_ind; cbn beta.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
forall y : Y, g (cofib f y) = g (cf_apex f)
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
{b : g (cf_apex f) = g (cf_apex f) &
forall x : X,
transport (fun x0 : Cofiber f => g x0 = g (cf_apex f)) 
  (cfglue f x) (?Goal (f x)) =
b}
  -
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
forall y : Y, g (cofib f y) = g (cf_apex f) rapply (conn_map_elim n f).
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
forall a : X, g (cofib f (f a)) = g (cf_apex f)
    intros x.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
x: X
g (cofib f (f x)) = g (cf_apex f)
    exact (ap g (cfglue f x)).
  -
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
{b : g (cf_apex f) = g (cf_apex f) &
forall x : X,
transport (fun x0 : Cofiber f => g x0 = g (cf_apex f)) 
  (cfglue f x)
  (conn_map_elim (Tr n) f (fun b0 : Y => g (cofib f b0) = g (cf_apex f))
     (fun x0 : X => ap g (cfglue f x0)) (f x)) =
b} exists idpath.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
forall x : X,
transport (fun x0 : Cofiber f => g x0 = g (cf_apex f)) 
  (cfglue f x)
  (conn_map_elim (Tr n) f (fun b : Y => g (cofib f b) = g (cf_apex f))
     (fun x0 : X => ap g (cfglue f x0)) (f x)) =
1
    intros x.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
x: X
transport (fun x0 : Cofiber f => g x0 = g (cf_apex f)) 
  (cfglue f x)
  (conn_map_elim (Tr n) f (fun b : Y => g (cofib f b) = g (cf_apex f))
     (fun x0 : X => ap g (cfglue f x0)) (f x)) =
1
    transport_paths Fl.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
x: X
conn_map_elim (Tr n) f (fun b : Y => g (cofib f b) = g (cf_apex f))
  (fun x0 : X => ap g (cfglue f x0)) (f x) =
ap g (cfglue f x) @ 1
    rhs napply concat_p1.
n: trunc_index
X, Y: Type
f: X -> Y
fc: IsConnMap (Tr n) f
C: Type
H': In (Tr n.+1) C
g: Cofiber f -> C
x: X
conn_map_elim (Tr n) f (fun b : Y => g (cofib f b) = g (cf_apex f))
  (fun x0 : X => ap g (cfglue f x0)) (f x) =
ap g (cfglue f x)
    napply conn_map_comp.
Defined.

(** ** Comparison of fibers and cofibers *)

Definition fiber_to_path_cofiber {X Y : Type} (f : X -> Y) (y : Y)
  : hfiber f y -> cofib f y = cf_apex f.
X, Y: Type
f: X -> Y
y: Y
hfiber f y -> cofib f y = cf_apex f
Proof.
X, Y: Type
f: X -> Y
y: Y
hfiber f y -> cofib f y = cf_apex f
  intros [x p].
X, Y: Type
f: X -> Y
y: Y
x: X
p: f x = y
cofib f y = cf_apex f
  lhs_V napply (ap (cofib f) p).
X, Y: Type
f: X -> Y
y: Y
x: X
p: f x = y
cofib f (f x) = cf_apex f
  apply cfglue.
Defined.

(** Blakers-Massey implies that the comparison map is highly connected.  Here we assume that [X] is merely inhabited.  There is a variant that instead assumes that [f] is surjective, with the same proof except that [blakers_massey_po] is used. *)
Definition isconnected_fiber_to_cofiber `{Univalence}
  (n m : trunc_index) {X Y : Type} {ac : IsConnected m.+1 X}
  (f : X -> Y) {fc : IsConnMap n f} (y : Y)
  : IsConnMap (m +2+ n).-1 (fiber_to_path_cofiber f y).
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
y: Y
IsConnMap (Tr (m +2+ n).-1) (fiber_to_path_cofiber f y)
Proof.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
y: Y
IsConnMap (Tr (m +2+ n).-1) (fiber_to_path_cofiber f y)
  (* It's enough to check the connectivity of [functor_sigma idmap (fiber_to_path_cofiber f)]. *)
  revert y; snapply conn_map_fiber.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnMap (Tr (m +2+ n).-1) (functor_sigma idmap (fiber_to_path_cofiber f))
  (* We precompose with the equivalence [X <~> { y : Y & hfiber f y }]. *)
  rapply (cancelR_conn_map _ (equiv_fibration_replacement _)).
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnMap (Tr (m +2+ n).-1)
  (fun x : X =>
   functor_sigma idmap (fiber_to_path_cofiber f)
     (equiv_fibration_replacement f x))
  (* The Sigma-type [{ y : Y & cofib f y = cf_apex f}] in the codomain is the fiber of the map [cofib f], and so it is equivalent to the pullback of the cospan in the pushout square defining [Cofiber f].  We postcompose with this equivalence. *)
  snapply (cancelL_equiv_conn_map _ _ (equiv_pullback_unit_hfiber _ _)^-1%equiv).
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnMap (Tr (m +2+ n).-1)
  ((equiv_pullback_unit_hfiber (cofib f) pushr)^-1%equiv
   o (fun x : X =>
      functor_sigma idmap (fiber_to_path_cofiber f)
        (equiv_fibration_replacement f x)))
  (* The composite is homotopic to the map from [blakers_massey_po], with the only difference being an extra [1 @ _]. *)
  snapply conn_map_homotopic.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
X -> Pullback (cofib f) pushr
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
?f ==
(fun x : X =>
 (equiv_pullback_unit_hfiber (cofib f) pushr)^-1%equiv
   ((fun x0 : X =>
     functor_sigma idmap (fiber_to_path_cofiber f)
       (equiv_fibration_replacement f x0))
      x))
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
IsConnMap (Tr (m +2+ n).-1) ?f
  3: rapply blakers_massey_po'.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
pullback_corec pglue ==
(fun x : X =>
 (equiv_pullback_unit_hfiber (cofib f) pushr)^-1%equiv
   ((fun x0 : X =>
     functor_sigma idmap (fiber_to_path_cofiber f)
       (equiv_fibration_replacement f x0))
      x))
  (* Use [compute.] to see the details of the goal. *)
  intros x.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
x: X
pullback_corec pglue x =
(equiv_pullback_unit_hfiber (cofib f) pushr)^-1%equiv
  (functor_sigma idmap (fiber_to_path_cofiber f)
     (equiv_fibration_replacement f x))
  apply (ap (fun z => (f x; tt; z))).
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
x: X
pglue x =
transport (fun x0 : Y => cofib f x0 = pushr tt)
  (eisretr 1%equiv
     (functor_sigma idmap (fiber_to_path_cofiber f)
        (equiv_fibration_replacement f x)).1)^
  (functor_sigma idmap (fiber_to_path_cofiber f)
     (equiv_fibration_replacement f x)).2
  unfold fiber_to_path_cofiber; simpl.
H: Univalence
n, m: trunc_index
X, Y: Type
ac: IsConnected (Tr m.+1) X
f: X -> Y
fc: IsConnMap (Tr n) f
x: X
pglue x = 1 @ cfglue f x
  symmetry; apply concat_1p.
Defined.

(** This lets us prove a converse to [isconnected_cofiber] when [X] is 1-connected. *)
Definition isconnmap_isconnected_cofiber `{Univalence}
  (n : trunc_index) {X Y : Type} `{IsConnected 1 X}
  (f : X -> Y) `{IsConnected n.+1 (Cofiber f)}
  : IsConnMap n f.
H: Univalence
n: trunc_index
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
H1: IsConnected (Tr n.+1) (Cofiber f)
IsConnMap (Tr n) f
Proof.
H: Univalence
n: trunc_index
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
H1: IsConnected (Tr n.+1) (Cofiber f)
IsConnMap (Tr n) f
  simple_induction n n IHn.
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
IsConnected (Tr (-1)) (Cofiber f) -> IsConnMap (Tr (-2)) f
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
n: trunc_index
IHn: IsConnected (Tr n.+1) (Cofiber f) -> IsConnMap (Tr n) f
IsConnected (Tr n.+2) (Cofiber f) -> IsConnMap (Tr n.+1) f
  -
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
IsConnected (Tr (-1)) (Cofiber f) -> IsConnMap (Tr (-2)) f exact _.
  -
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
n: trunc_index
IHn: IsConnected (Tr n.+1) (Cofiber f) -> IsConnMap (Tr n) f
IsConnected (Tr n.+2) (Cofiber f) -> IsConnMap (Tr n.+1) f intros conn_cof y.
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
n: trunc_index
IHn: IsConnected (Tr n.+1) (Cofiber f) -> IsConnMap (Tr n) f
conn_cof: IsConnected (Tr n.+2) (Cofiber f)
y: Y
IsConnected (Tr n.+1) (hfiber f y)
    rapply (isconnected_conn_map_isconnected (n.+1) (fiber_to_path_cofiber f y)).
H: Univalence
X, Y: Type
H0: IsConnected (Tr 1) X
f: X -> Y
n: trunc_index
IHn: IsConnected (Tr n.+1) (Cofiber f) -> IsConnMap (Tr n) f
conn_cof: IsConnected (Tr n.+2) (Cofiber f)
y: Y
IsConnMap (Tr n.+1) (fiber_to_path_cofiber f y)
    rapply (isconnected_fiber_to_cofiber n 0).
Defined.