Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids Basics.Trunc Basics.Equivalences.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 isconnnected_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.
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,
(fun x : Cofiber f => g x = g (cf_apex f)) (cofib f y)
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
: (fun x : Cofiber f => g x = g (cf_apex f))
    (cf_apex f) &
forall x : X,
transport (fun x0 : Cofiber f => g x0 = g (cf_apex f))
  (cfglue f x) (?g (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,
(fun x : Cofiber f => g x = g (cf_apex f)) (cofib f y) 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
: (fun x : Cofiber f => g x = g (cf_apex f))
    (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 =>
      (fun x0 : Cofiber f => g x0 = g (cf_apex f))
        (cofib f b0))
     (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 x : Cofiber f => g x = 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 x : X => ap g (cfglue f x)) (f x)) = 1
    lhs snapply 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
(ap g (cfglue f x))^ @
conn_map_elim (Tr n) f
  (fun b : Y => g (cofib f b) = g (cf_apex f))
  (fun x : X => ap g (cfglue f x)) (f x) = 1
    apply moveR_Vp.
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 x : X => ap g (cfglue f x)) (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 x : X => ap g (cfglue f x)) (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. *)
Definition isconnected_fiber_to_cofiber `{Univalence}
  (n m : trunc_index) {X Y : Type} {ac : IsConnected m.+1 X}
  (f : X -> Y) {fc : IsConnMap n.+1 f} (y : Y)
  : IsConnMap (m +2+ n) (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.+1) f
y: Y
IsConnMap (Tr (m +2+ n)) (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.+1) f
y: Y
IsConnMap (Tr (m +2+ n)) (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.+1) f
IsConnMap (Tr (m +2+ n))
  (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.+1) f
IsConnMap (Tr (m +2+ n))
  (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.+1) f
IsConnMap (Tr (m +2+ n))
  ((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.+1) 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.+1) 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.+1) f
IsConnMap (Tr (m +2+ n)) ?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.+1) 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.+1) 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.+1) f
x: X
pglue x =
transport (fun x : Y => cofib f x = 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.+1) f
x: X
pglue x = 1 @ cfglue f x
  symmetry; apply concat_1p.
Defined.