add missing coherence for TwoOneCat

We were missing the bifunctor coherence for composition. This lets us prove the exachange law in a (2,1)-category. Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Mar 13, 2024 · bc0a585 · bc0a585
1 parent 2bd6c4a
commit bc0a585
Show file tree

Hide file tree

Showing 3 changed files with 32 additions and 2 deletions.
diff --git a/theories/Pointed/Core.v b/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 _)^).

diff --git a/theories/WildCat/TwoOneCat.v b/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') (s : g' $== g''),
+    (g' $@L p) $@ (s $@R f') $== (s $@R f) $@ (g'' $@L p);
 
   (** 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,23 @@ 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.
+
+(** *** 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.
+  refine ((_ $@@ _) $@ _).
+  1: rapply fmap_comp.
+  1: rapply fmap_comp.
+  refine (cat_assoc _ _ _ $@ _).
+  refine (_ $@ (cat_assoc _ _ _)^$).
+  nrefine (_ $@L _).
+  refine (_ $@ cat_assoc _ _ _).
+  refine ((cat_assoc _ _ _)^$ $@ _).
+  nrefine (_ $@R _).
+  symmetry.
+  apply bifunctor_coh_comp.
+Defined.
diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v
@@ -149,7 +149,9 @@ 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.
+    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.