(* -*- mode: coq; mode: visual-line -*- *)

(** * Mapping Cylinders *)

Require Import HoTT.Basics Cubical.DPath Cubical.PathSquare.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Colimits.Pushout.
Local Open Scope path_scope.

(** As in topology, the mapping cylinder of a function [f : A -> B] is a way to replace it with an equivalent cofibration (dually to how [hfiber] replaces it with an equivalent fibration).  We can't talk *internally* in type theory about cofibrations, but we can say metatheoretically what they are: functions with the isomorphism extension property.  So while we can't literally say "let [f] be a cofibration" we can do a mostly equivalent thing and say "let [f] be a map and consider its mapping cylinder".  Replacing a map by a cofibration can be useful because it allows us to make more equalities true definitionally. *)

(** ** Definitions *)

(** We define the mapping cylinder as the pushout of [f] and an identity map.  Peter Lumsdaine has given a definition of HIT mapping cylinders that are dependent on the codomain, so that the second factor is not just an equivalence but a trivial fibration.  However, at the moment we don't have a need for that.  *)

Definition Cyl {A B : Type} (f : A -> B) : Type
  := Pushout idmap f.

Section MappingCylinder.
  Context {A B : Type} {f : A -> B}.

  Definition cyl (a : A) : Cyl f
    := pushl a.
  Definition cyr (b : B) : Cyl f
    := pushr b.

  Definition cyglue (a : A)
    : cyl a = cyr (f a)
    := pglue a.

  Section CylInd.
    Context (P : Cyl f -> Type)
            (cyla : forall a, P (cyl a))
            (cylb : forall b, P (cyr b))
            (cylg : forall a, DPath P (cyglue a) (cyla a) (cylb (f a))).

    Definition Cyl_ind : forall c, P c
      := Pushout_ind _ cyla cylb cylg.

    Definition Cyl_ind_beta_cyglue (a : A)
      : apD Cyl_ind (cyglue a) = cylg a
      := Pushout_ind_beta_pglue _ _ _ _ _.

  End CylInd.

  Section CylRec.
    Context {P : Type} (cyla : A -> P) (cylb : B -> P) (cylg : cyla == cylb o f).

    Definition Cyl_rec : Cyl f -> P
      := Pushout_rec _ cyla cylb cylg.

    Definition Cyl_rec_beta_cyglue (a : A)
      : ap Cyl_rec (cyglue a) = cylg a
      := Pushout_rec_beta_pglue _ _ _ _ _.

  End CylRec.

  Definition pr_cyl : Cyl f <~> B.
A, B: Type
f: A -> B
Cyl f <~> B
  Proof.
A, B: Type
f: A -> B
Cyl f <~> B
    (** Rather than adjointifying, we give all parts of the equivalence explicitly, so we can be sure of retaining the computational behavior of [eissect] and [eisretr].  However, it's easier to prove [eisadj] on the other side, so we reverse the equivalence first. *)
    symmetry.
A, B: Type
f: A -> B
B <~> Cyl f
    srapply Build_Equiv.
A, B: Type
f: A -> B
B -> Cyl f
A, B: Type
f: A -> B
IsEquiv ?equiv_fun
    1:apply cyr.
A, B: Type
f: A -> B
IsEquiv cyr
    srapply Build_IsEquiv.
A, B: Type
f: A -> B
Cyl f -> B
A, B: Type
f: A -> B
cyr o ?equiv_inv == idmap
A, B: Type
f: A -> B
?equiv_inv o cyr == idmap
A, B: Type
f: A -> B
forall x : B, ?eisretr (cyr x) = ap cyr (?eissect x)
    -
A, B: Type
f: A -> B
Cyl f -> B srapply Cyl_rec.
A, B: Type
f: A -> B
A -> B
A, B: Type
f: A -> B
B -> B
A, B: Type
f: A -> B
?cyla == ?cylb o f
      +
A, B: Type
f: A -> B
A -> B exact f.
      +
A, B: Type
f: A -> B
B -> B exact idmap.
      +
A, B: Type
f: A -> B
f == idmap o f reflexivity.
    -
A, B: Type
f: A -> B
cyr o Cyl_rec f idmap (fun x0 : A => 1) == idmap srapply Cyl_ind.
A, B: Type
f: A -> B
forall a : A,
(fun c : Cyl f =>
 (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c = idmap c)
  (cyl a)
A, B: Type
f: A -> B
forall b : B,
(fun c : Cyl f =>
 (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c = idmap c)
  (cyr b)
A, B: Type
f: A -> B
forall a : A,
DPath
  (fun c : Cyl f =>
   (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
   idmap c) (cyglue a) (?cyla a) (?cylb (f a))
      +
A, B: Type
f: A -> B
forall a : A,
(fun c : Cyl f =>
 (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c = idmap c)
  (cyl a) intros a; cbn.
A, B: Type
f: A -> B
a: A
cyr (Cyl_rec f idmap (fun x0 : A => 1) (cyl a)) =
cyl a
        symmetry; apply cyglue.
      +
A, B: Type
f: A -> B
forall b : B,
(fun c : Cyl f =>
 (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c = idmap c)
  (cyr b) intros b; reflexivity.
      +
A, B: Type
f: A -> B
forall a : A,
DPath
  (fun c : Cyl f =>
   (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
   idmap c) (cyglue a)
  ((fun a0 : A =>
    (cyglue a0)^
    :
    (fun c : Cyl f =>
     (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
     idmap c) (cyl a0)) a) ((fun b : B => 1) (f a)) intros a; cbn.
A, B: Type
f: A -> B
a: A
transport
  (fun c : Cyl f =>
   cyr (Cyl_rec f idmap (fun x0 : A => 1) c) = c)
  (cyglue a) (cyglue a)^ = 1
        apply dp_paths_FFlr.
A, B: Type
f: A -> B
a: A
((ap cyr
    (ap (Cyl_rec f idmap (fun x0 : A => 1)) (cyglue a)))^ @
 (cyglue a)^) @ cyglue a = 1
        rewrite Cyl_rec_beta_cyglue.
A, B: Type
f: A -> B
a: A
((ap cyr 1)^ @ (cyglue a)^) @ cyglue a = 1
        apply concat_pV_p.
    -
A, B: Type
f: A -> B
Cyl_rec f idmap (fun x0 : A => 1) o cyr == idmap intros b; reflexivity.
    -
A, B: Type
f: A -> B
forall x : B,
Cyl_ind
  (fun c : Cyl f =>
   (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
   idmap c)
  (fun a : A =>
   (cyglue a)^
   :
   (fun c : Cyl f =>
    (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
    idmap c) (cyl a)) (fun b : B => 1)
  (fun a : A =>
   (let X :=
      fun (p : cyl a = cyr (f a))
        (q : cyr
               (Cyl_rec f idmap (fun x0 : A => 1)
                  (cyl a)) = cyl a)
        (r : cyr
               (Cyl_rec f idmap (fun x0 : A => 1)
                  (cyr (f a))) = cyr (f a)) =>
      equiv_fun (dp_paths_FFlr p q r) in
    X (cyglue a) (cyglue a)^ 1
      (internal_paths_rew_r
         (fun
            p : Cyl_rec f idmap (fun x0 : A => 1)
                  (cyl a) =
                Cyl_rec f idmap (fun x0 : A => 1)
                  (cyr (f a)) =>
          ((ap cyr p)^ @ (cyglue a)^) @ cyglue a = 1)
         (concat_pV_p 1 (cyglue a))
         (Cyl_rec_beta_cyglue f idmap
            (fun x0 : A => 1) a)))
   :
   DPath
     (fun c : Cyl f =>
      (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
      idmap c) (cyglue a)
     ((fun a0 : A =>
       (cyglue a0)^
       :
       (fun c : Cyl f =>
        (cyr o Cyl_rec f idmap (fun x0 : A => 1)) c =
        idmap c) (cyl a0)) a) ((fun b : B => 1) (f a)))
  (cyr x) =
ap cyr
  (((fun b : B => 1)
    :
    Cyl_rec f idmap (fun x0 : A => 1) o cyr == idmap)
     x) intros b; reflexivity.
  Defined.

  Definition ap_pr_cyl_cyglue (a : A)
    : ap pr_cyl (cyglue a) = 1
    := Cyl_rec_beta_cyglue _ _ _ a.

  (** The original map [f] factors definitionally through [Cyl f]. *)
  Definition pr_cyl_cyl (a : A) : pr_cyl (cyl a) = f a
    := 1.

End MappingCylinder.

(** Sometimes we have to specify the map explicitly. *)
Definition cyl' {A B} (f : A -> B) : A -> Cyl f := cyl.
Definition pr_cyl' {A B} (f : A -> B) : Cyl f -> B := pr_cyl.

(** ** Functoriality *)

Section FunctorCyl.
  Context {A B A' B': Type} {f : A -> B} {f' : A' -> B'}
          {ga : A -> A'} {gb : B -> B'}
          (g : f' o ga == gb o f).

  Definition functor_cyl : Cyl f -> Cyl f'.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
Cyl f -> Cyl f'
  Proof.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
Cyl f -> Cyl f'
    srapply Cyl_rec.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
A -> Cyl f'
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
B -> Cyl f'
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
?cyla == ?cylb o f
    -
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
A -> Cyl f' exact (cyl o ga).
    -
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
B -> Cyl f' exact (cyr o gb).
    -
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
cyl o ga == cyr o gb o f intros a.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
cyl (ga a) = cyr (gb (f a))
      refine (_ @ ap cyr (g a)).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
cyl (ga a) = cyr (f' (ga a))
      exact (cyglue (ga a)).
  Defined.

  Definition ap_functor_cyl_cyglue (a : A)
    : ap functor_cyl (cyglue a) = cyglue (ga a) @ ap cyr (g a)
    := Cyl_rec_beta_cyglue _ _ _ a.

  (** The benefit of passing to the mapping cylinder is that it makes a square commute definitionally. *)
  Definition functor_cyl_cyl (a : A) : cyl (ga a) = functor_cyl (cyl a)
    := 1.

  (** The other square also commutes, though not definitionally. *)
  Definition pr_functor_cyl (c : Cyl f)
    : pr_cyl (functor_cyl c) = gb (pr_cyl c)
    := ap (pr_cyl o functor_cyl) (eissect pr_cyl c)^.

  Definition pr_functor_cyl_cyl (a : A)
    : pr_functor_cyl (cyl a) = g a.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
pr_functor_cyl (cyl a) = g a
  Proof.
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
pr_functor_cyl (cyl a) = g a
    (** Here we need [eissect pr_cyl (cyl a)] to compute. *)
    refine (ap _ (inv_V _) @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap (fun x : Cyl f => pr_cyl (functor_cyl x))
  (cyglue a) = g a
    refine (ap_compose functor_cyl pr_cyl (cyglue a) @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap pr_cyl (ap functor_cyl (cyglue a)) = g a
    refine (ap _ (ap_functor_cyl_cyglue a) @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap pr_cyl (cyglue (ga a) @ ap cyr (g a)) = g a
    refine (ap_pp _ _ _ @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap pr_cyl (cyglue (ga a)) @ ap pr_cyl (ap cyr (g a)) =
g a
    refine (whiskerR (ap_pr_cyl_cyglue (ga a)) _ @ concat_1p _ @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap pr_cyl (ap cyr (g a)) = g a
    refine ((ap_compose cyr _ (g a))^ @ _).
A, B, A', B': Type
f: A -> B
f': A' -> B'
ga: A -> A'
gb: B -> B'
g: f' o ga == gb o f
a: A
ap (fun x : B' => pr_cyl (cyr x)) (g a) = g a
    apply ap_idmap.
  Defined.

End FunctorCyl.

(** ** Coequalizers *)

(** A particularly useful application is to replace a map of coequalizers with one where both squares commute definitionally. *)

Section CylCoeq.
  Context {B A f g B' A' f' g'}
          {h : B -> B'} {k : A -> A'}
          (p : k o f == f' o h) (q : k o g == g' o h).

  Definition CylCoeq : Type
    := Coeq (functor_cyl p) (functor_cyl q).

  Definition cyl_cylcoeq : Coeq f g -> CylCoeq
    := functor_coeq cyl cyl (functor_cyl_cyl p) (functor_cyl_cyl q).

  Definition ap_cyl_cylcoeq_cglue (b : B)
    : ap cyl_cylcoeq (cglue b) = cglue (cyl b).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
ap cyl_cylcoeq (cglue b) = cglue (cyl b)
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
ap cyl_cylcoeq (cglue b) = cglue (cyl b)
    etransitivity.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
ap cyl_cylcoeq (cglue b) = ?Goal
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
?Goal = cglue (cyl b)
    1:rapply functor_coeq_beta_cglue.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
b: B
(ap coeq (functor_cyl_cyl p b) @ cglue (cyl b)) @
ap coeq (functor_cyl_cyl q b)^ = cglue (cyl b)
    exact (concat_p1 _ @ concat_1p _).
  Defined.

  Definition pr_cylcoeq : CylCoeq <~> Coeq f' g'
    := equiv_functor_coeq pr_cyl pr_cyl (pr_functor_cyl p) (pr_functor_cyl q).

  Definition ap_pr_cylcoeq_cglue (x : Cyl h)
    : PathSquare (ap pr_cylcoeq (cglue x)) (cglue (pr_cyl x))
                 (ap coeq (pr_functor_cyl p x))
                 (ap coeq (pr_functor_cyl q x)).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
x: Cyl h
PathSquare (ap pr_cylcoeq (cglue x))
  (cglue (pr_cyl x)) (ap coeq (pr_functor_cyl p x))
  (ap coeq (pr_functor_cyl q x))
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
x: Cyl h
PathSquare (ap pr_cylcoeq (cglue x))
  (cglue (pr_cyl x)) (ap coeq (pr_functor_cyl p x))
  (ap coeq (pr_functor_cyl q x))
    apply sq_path.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
x: Cyl h
ap pr_cylcoeq (cglue x) @ ap coeq (pr_functor_cyl q x) =
ap coeq (pr_functor_cyl p x) @ cglue (pr_cyl x)
    apply moveR_pM.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
x: Cyl h
ap pr_cylcoeq (cglue x) =
(ap coeq (pr_functor_cyl p x) @ cglue (pr_cyl x)) @
(ap coeq (pr_functor_cyl q x))^
    rewrite <- (ap_V coeq).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
x: Cyl h
ap pr_cylcoeq (cglue x) =
(ap coeq (pr_functor_cyl p x) @ cglue (pr_cyl x)) @
ap coeq (pr_functor_cyl q x)^
    rapply functor_coeq_beta_cglue.
  Defined.

  Definition pr_cyl_cylcoeq
    : functor_coeq h k p q == pr_cylcoeq o cyl_cylcoeq.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
functor_coeq h k p q == pr_cylcoeq o cyl_cylcoeq
  Proof.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
functor_coeq h k p q == pr_cylcoeq o cyl_cylcoeq
    intros c.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
functor_coeq h k p q c = pr_cylcoeq (cyl_cylcoeq c)
    refine (_ @ functor_coeq_compose cyl cyl (functor_cyl_cyl p) (functor_cyl_cyl q)
              pr_cyl pr_cyl (pr_functor_cyl p) (pr_functor_cyl q) c).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
functor_coeq h k p q c =
functor_coeq (fun x : B => pr_cyl (cyl x))
  (fun x : A => pr_cyl (cyl x))
  (fun b : B =>
   ap pr_cyl (functor_cyl_cyl p b) @
   pr_functor_cyl p (cyl b))
  (fun b : B =>
   ap pr_cyl (functor_cyl_cyl q b) @
   pr_functor_cyl q (cyl b)) c
    srapply functor_coeq_homotopy.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
h == (fun x : B => pr_cyl (cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
k == (fun x : A => pr_cyl (cyl x))
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
forall b : B,
?s (f b) @
(fun b0 : B =>
 ap pr_cyl (functor_cyl_cyl p b0) @
 pr_functor_cyl p (cyl b0)) b = p b @ ap f' (?r b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
forall b : B,
?s (g b) @
(fun b0 : B =>
 ap pr_cyl (functor_cyl_cyl q b0) @
 pr_functor_cyl q (cyl b0)) b = q b @ ap g' (?r b)
    1-2:reflexivity.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
forall b : B,
(fun x0 : A => 1) (f b) @
(fun b0 : B =>
 ap pr_cyl (functor_cyl_cyl p b0) @
 pr_functor_cyl p (cyl b0)) b =
p b @ ap f' ((fun x0 : B => 1) b)
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
forall b : B,
(fun x0 : A => 1) (g b) @
(fun b0 : B =>
 ap pr_cyl (functor_cyl_cyl q b0) @
 pr_functor_cyl q (cyl b0)) b =
q b @ ap g' ((fun x0 : B => 1) b)
    all:intros b; cbn.
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
b: B
1 @ (1 @ pr_functor_cyl p (cyl b)) = p b @ 1
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
b: B
1 @ (1 @ pr_functor_cyl q (cyl b)) = q b @ 1
    all:refine (concat_1p _ @ concat_1p _ @ _ @ (concat_p1 _)^).
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
b: B
pr_functor_cyl p (cyl b) = p b
B, A: Type
f, g: B -> A
B', A': Type
f', g': B' -> A'
h: B -> B'
k: A -> A'
p: k o f == f' o h
q: k o g == g' o h
c: Coeq f g
b: B
pr_functor_cyl q (cyl b) = q b
    all:apply pr_functor_cyl_cyl.
  Defined.

End CylCoeq.