Symmetric Monoidal Categories and Twist Construction

We define give a definition of symmetric monoidal categories and develop
what we term the "twist construction" for building examples.

The twist construction takes a symmetric braiding, a twist map A(BC)
-> B(AC), and some extra axioms and produces a symmetric monoidal
category.

We give the cartesian symmetric monoidal structure as an application.

Signed-off-by: Ali Caglayan <[email protected]>

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 *)

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 *)