From 07a55d8d93abedcbd7cb3fe5875aba48fdaea6e6 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Tue, 12 Mar 2024 22:08:39 +0100
Subject: [PATCH] add whiskering lemmas and make proof of exchange more
 reasable with comments

<!-- ps-id: 7a8dab5b-25d0-4e0d-8341-677ae85964be -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Pointed/Core.v      |  2 +-
 theories/WildCat/TwoOneCat.v | 34 ++++++++++++++++++++++++++--------
 theories/WildCat/Universe.v  |  5 +++--
 3 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v
index 6048fb2f3c5..0f28c746493 100644
--- a/theories/Pointed/Core.v
+++ b/theories/Pointed/Core.v
@@ -647,7 +647,7 @@ Proof.
   - intros A B C f g h k p q.
     snrapply Build_pHomotopy.
     + intros x.
-      exact (concat_Ap q _).
+      exact (concat_Ap q _)^.
     + by pelim p f g q h k.
   - intros A B C D f g r1 r2 s1.
     srapply Build_pHomotopy.
diff --git a/theories/WildCat/TwoOneCat.v b/theories/WildCat/TwoOneCat.v
index a9a87c4fbb4..06716d1ae9a 100644
--- a/theories/WildCat/TwoOneCat.v
+++ b/theories/WildCat/TwoOneCat.v
@@ -10,9 +10,9 @@ Class Is21Cat (A : Type) `{Is1Cat A, !Is3Graph A} :=
   is1gpd_hom : forall (a b : A), Is1Gpd (a $-> b) ;
   is1functor_postcomp : forall (a b c : A) (g : b $-> c), Is1Functor (cat_postcomp a g) ;
   is1functor_precomp : forall (a b c : A) (f : a $-> b), Is1Functor (cat_precomp c f) ;
-  bifunctor_coh_comp : forall {a b c : A} {f f' : a $-> b}  {g' g'' : b $-> c}
-    (p : f $== f') (s : g' $== g''),
-    (g' $@L p) $@ (s $@R f') $== (s $@R f) $@ (g'' $@L p);
+  bifunctor_coh_comp : forall {a b c : A} {f f' : a $-> b}  {g g' : b $-> c}
+    (p : f $== f') (p' : g $== g'),
+    (p' $@R f) $@ (g' $@L p) $== (g $@L p) $@ (p' $@R f') ;
 
   (** Naturality of the associator in each variable separately *)
   is1natural_cat_assoc_l : forall (a b c d : A) (f : a $-> b) (g : b $-> c),
@@ -54,6 +54,22 @@ Global Existing Instance is1natural_cat_assoc_r.
 Global Existing Instance is1natural_cat_idl.
 Global Existing Instance is1natural_cat_idr.
 
+(** *** Whiskering functoriality *)
+
+Definition cat_postwhisker_pp {A} `{Is21Cat A} {a b c : A}
+  {f g h : a $-> b} (k : b $-> c) (p : f $== g) (q : g $== h)
+  : k $@L (p $@ q) $== (k $@L p) $@ (k $@L q).
+Proof.
+  rapply fmap_comp.
+Defined.
+
+Definition cat_prewhisker_pp {A} `{Is21Cat A} {a b c : A}
+  {f g h : b $-> c} (k : a $-> b) (p : f $== g) (q : g $== h)
+  : (p $@ q) $@R k $== (p $@R k) $@ (q $@R k).
+Proof.
+  rapply fmap_comp.
+Defined.
+
 (** *** Exchange law *)
 
 Definition cat_exchange {A : Type} `{Is21Cat A} {a b c : A}
@@ -61,15 +77,17 @@ Definition cat_exchange {A : Type} `{Is21Cat A} {a b c : A}
   (p : f $== f') (q : f' $== f'') (r : g $== g') (s : g' $== g'')
   : (p $@ q) $@@ (r $@ s) $== (p $@@ r) $@ (q $@@ s).
 Proof.
-  refine ((_ $@@ _) $@ _).
-  1: rapply fmap_comp.
-  1: rapply fmap_comp.
-  refine (cat_assoc _ _ _ $@ _).
+  unfold "$@@".
+  (** We use the distributivity of [$@R] and [$@L] in a (2,1)-category (since they are functors) to see that we have the same dadta on both sides of the 3-morphism. *)
+  nrefine ((_ $@L cat_prewhisker_pp _ _ _ ) $@ _).
+  nrefine ((cat_postwhisker_pp _ _ _ $@R _) $@ _).
+  (** Now we reassociate and whisker on the left and right. *)
+  nrefine (cat_assoc _ _ _ $@ _).
   refine (_ $@ (cat_assoc _ _ _)^$).
   nrefine (_ $@L _).
   refine (_ $@ cat_assoc _ _ _).
   refine ((cat_assoc _ _ _)^$ $@ _).
   nrefine (_ $@R _).
-  symmetry.
+  (** Finally we are left with the bifunctoriality condition for left and right whiskering which is part of the data of the (2,1)-cat. *)
   apply bifunctor_coh_comp.
 Defined.
diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v
index 87e1f1c9bb4..c968aa74c75 100644
--- a/theories/WildCat/Universe.v
+++ b/theories/WildCat/Universe.v
@@ -149,8 +149,9 @@ Defined.
 Global Instance is21cat_type : Is21Cat Type.
 Proof.
   snrapply Build_Is21Cat.
-  1-4,6-7: exact _.
-  - intros a b c f g h k p q x. cbn.
+  1-4, 6-7: exact _.
+  - intros a b c f g h k p q x; cbn.
+    symmetry.
     apply concat_Ap.
   - intros a b c d f g h i p x; cbn.
     exact (concat_p1 _ @ ap_compose _ _ _ @ (concat_1p _)^).