Merge pull request #1897 from Alizter/ps/rr/add_missing_coherence_for_twoonecat

add missing coherence for TwoOneCat

Author: Alizter

theories/Pointed/Core.v

@@ -644,6 +644,11 @@ Proof.
       srapply Build_pHomotopy.
       1: reflexivity.
       by pelim f p q i g h.
+  - intros A B C f g h k p q.
+    snrapply Build_pHomotopy.
+    + intros x.
+      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.
     1: exact (fun _ => concat_p1 _ @ (concat_1p _)^).

theories/WildCat/TwoOneCat.v

@@ -1,4 +1,4 @@
-Require Import Basics.Overture.
+Require Import Basics.Overture Basics.Tactics.
 Require Import WildCat.Core.
 Require Import WildCat.NatTrans.
 
@@ -10,6 +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') (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),
@@ -50,3 +53,41 @@ Global Existing Instance is1natural_cat_assoc_m.
 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}
+  {f f' f'' : a $-> b} {g g' g'' : b $-> c}
+  (p : f $== f') (q : f' $== f'') (r : g $== g') (s : g' $== g'')
+  : (p $@ q) $@@ (r $@ s) $== (p $@@ r) $@ (q $@@ s).
+Proof.
+  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 _).
+  (** 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.

theories/WildCat/Universe.v

@@ -149,7 +149,10 @@ Defined.
 Global Instance is21cat_type : Is21Cat Type.
 Proof.
   snrapply Build_Is21Cat.
-  1-6: exact _.
+  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 _)^).
   - intros a b f g p x; cbn.