Library HoTT.Diagrams.CommutativeSquares

Require Import Basics.Overture Basics.PathGroupoids.

Comutative squares

Commutative squares compose vertically.
A --f--> B | // | h comm g | // | V // V C --f'-> D | // | h' comm' g' | // | V // V E --f''> F
Lemma comm_square_comp {A B C D E F}
  {f : A → B} {f': C → D} {h : A → C} {g : B → D} (comm : f' o h == g o f)
  {f'': E → F} {h' : C → E} {g' : D → F} (comm' : f'' o h' == g' o f')
  : f'' o (h' o h) == (g' o g) o f.
Proof.
  intros x.
  path_via (g' (f' (h x))).
  apply ap, comm.
Defined.

Commutative squares compose horizontally.
A --k--> B --l--> C | // | // | f comm g comm h | // | // | V // V // V X --i--> Y --j--> Z

Lemma comm_square_comp' {A B C X Y Z : Type}
    {k : A → B} {l : B → C}
    {f : A → X} {g : B → Y} {h : C → Z}
    {i : X → Y} {j : Y → Z}
    (H : i o f == g o k) (K : j o g == h o l)
  : (j o i) o f == h o (l o k).
Proof.
  intros x.
  path_via (j (g (k x))).
  apply ap, H.
Defined.

Given any commutative square from f to f' whose verticals wA, wB are equivalences, the equiv_inv square from f' to f with verticals wA ^-1, wB ^-1 also commutes.
Lemma comm_square_inverse
  {A B : Type} {f : A → B}
  {A' B' : Type} {f' : A' → B'}
  {wA : A <~> A'} {wB : B <~> B'}
  (wf : f' o wA == wB o f)
: f o (wA ^-1) == (wB ^-1) o f'.
Proof.
  intros a'.
  path_via (wB ^-1 (wB (f (wA ^-1 a')))).
  - apply inverse, eissect.
  - apply ap, (concat (wf _)^).
    apply ap, eisretr.
Defined.

Up to naturality, the result of comm_square_inverse really is a retraction (aka left inverse);
Lemma comm_square_inverse_is_sect
  {A B : Type} {f : A → B}
  {A' B' : Type} {f' : A' → B'}
  (wA : A <~> A') (wB : B <~> B')
  (wf : f' o wA == wB o f) (a : A)
  : comm_square_comp wf (comm_square_inverse wf) a @ eissect wB (f a)
   = ap f (eissect wA a).
Proof.
  unfold comm_square_inverse, comm_square_comp; simpl.
  repeat apply (concat (concat_pp_p _ _ _)). apply moveR_Vp.
  transitivity (ap (wB ^-1 o wB) (ap f (eissect wA a)) @ eissect wB (f a)).
  2: apply (concat (concat_Ap (eissect wB) _)). 2: apply ap, ap_idmap.
  apply (concat (concat_p_pp _ _ _)), whiskerR.
  apply (concat (ap_pp (wB ^-1) _ _)^), (concatR (ap_compose wB _ _)^).
  apply ap, (concat (concat_pp_p _ _ _)), moveR_Vp.
  path_via (ap (f' o wA) (eissect wA a) @ wf a).
  - apply whiskerR. apply (concatR (ap_compose wA f' _)^).
    apply ap, eisadj.
  - apply (concat (concat_Ap wf _)).
    apply whiskerL, (ap_compose f wB).
Defined.

and similarly, comm_square_inverse is a section (aka right equiv_inv).
Lemma comm_square_inverse_is_retr
  {A B : Type} {f : A → B}
  {A' B' : Type} {f' : A' → B'}
  (wA : A <~> A') (wB : B <~> B')
  (wf : f' o wA == wB o f) (a : A')
  : comm_square_comp (comm_square_inverse wf) wf a @ eisretr wB (f' a)
  = ap f' (eisretr wA a).
Proof.
  unfold comm_square_inverse, comm_square_comp; simpl.
  rewrite !ap_pp.
  rewrite <- !concat_pp_p.
  rewrite concat_pp_p.
  set (p := (ap wB (ap (wB ^-1) (ap f' (eisretr wA a)))
            @ eisretr wB (f' a))).
  path_via ((eisretr wB _)^ @ p).
  - apply whiskerR.
    apply moveR_pM.
    path_via ((eisretr wB (f' (wA (wA ^-1 a))))^ @
      ap (wB o wB ^-1) (wf ((wA ^-1) a))).
    + rewrite ap_V, <- eisadj.
      transitivity (ap idmap (wf ((wA ^-1) a))
                       @ (eisretr wB (wB (f ((wA ^-1) a))))^).
      × apply whiskerR, inverse, ap_idmap.
      × apply (concat_Ap (fun b' ⇒ (eisretr wB b')^) _).
    + apply ap.
      rewrite ap_compose, !ap_V.
      apply inverse, inv_V.
  - apply moveR_Vp.
    subst p.
    rewrite <- ap_compose.
    path_via (eisretr wB _ @ ap idmap (ap f' (eisretr wA a))).
    + apply (concat_Ap (eisretr wB) _).
    + apply ap, ap_idmap.
Defined.