Merge pull request #1915 from Alizter/wip-symmetric-monoidal

Symmetric Monoidal Categories
HoTT · Apr 24, 2024 · 6fa56dc · 6fa56dc
2 parents 08cfa11 + 6eefc6d
commit 6fa56dc
Show file tree

Hide file tree

Showing 4 changed files with 1,188 additions and 83 deletions.
diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
@@ -103,14 +103,14 @@ Defined.
 Definition fmap10_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $-> a1) (b : B)
-  : fmap11 F f (Id b) $== fmap10 F f b 
+  : fmap11 F f (Id b) $== fmap10 F f b
   := (fmap_id _ _ $@R _) $@ cat_idl _.
 
 (** [fmap11] with left map the identity gives [fmap01]. *)
 Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   (a : A) {b0 b1 : B} (g : b0 $-> b1)
-  : fmap11 F (Id a) g $== fmap01 F a g 
+  : fmap11 F (Id a) g $== fmap01 F a g
   := (_ $@L fmap_id _ _) $@ cat_idr _.
 
 (** 2-functorial action *)

diff --git a/theories/WildCat/Coproducts.v b/theories/WildCat/Coproducts.v
@@ -2,7 +2,8 @@ Require Import Basics.Overture Basics.Tactics Basics.Decidable.
 Require Import Types.Bool.
 Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans
                WildCat.Opposite WildCat.Products WildCat.Universe
-               WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat.
+               WildCat.Yoneda WildCat.ZeroGroupoid WildCat.PointedCat
+               WildCat.Monoidal.
 
 (** * Categories with coproducts *)
 
@@ -226,7 +227,7 @@ Lemma cate_coprod_assoc {A : Type} `{HasEquivs A}
   : cat_bincoprod x (cat_bincoprod y z)
     $<~> cat_bincoprod (cat_bincoprod x y) z.
 Proof.
-  exact (@cate_binprod_assoc A^op _ _ _ _ _ e x y z)^-1$.
+  exact (@associator_binprod A^op _ _ _ _ _ e x y z)^-1$.
 Defined.
 
 (** *** Binary coproduct functor *)