diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index fceb2b43afb..f9cdaa63816 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -62,13 +62,36 @@ Definition fmap10 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   : (F a0 b) $-> (F a1 b)
   := fmap (flip F b) f.
 
+Global Instance iemap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $<~> a1) (b : B)
+  : CatIsEquiv (fmap10 F f b)
+  := iemap (flip F _) f.
+
+Definition emap10 {A B C : Type} `{HasEquivs A, Is1Cat B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  {a0 a1 : A} (f : a0 $<~> a1) (b : B)
+  : F a0 b $<~> F a1 b
+  := Build_CatEquiv (fmap10 F f b).
+
 (** [fmap] in the second argument *)
 Definition fmap01 {A B C : Type} `{IsGraph A, IsGraph B, IsGraph C}
   (F : A -> B -> C) `{!Is0Bifunctor F} (a : A) {b0 b1 : B} (g : b0 $-> b1)
   : F a b0 $-> F a b1
   := fmap (F a) g.
 
-(** There are two ways to [fmap] in both arguments of a bifunctor. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
+Global Instance iemap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (a : A) {b0 b1 : B} (g : b0 $<~> b1)
+  : CatIsEquiv (fmap01 F a g)
+  := iemap (F _) g.
+
+Definition emap01 {A B C : Type} `{Is1Cat A, HasEquivs B, HasEquivs C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
+  (a : A) {b0 b1 : B} (g : b0 $<~> b1)
+  : F a b0 $<~> F a b1
+  := Build_CatEquiv (fmap01 F a g).
+
 Definition fmap11 {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F} {a0 a1 : A} (f : a0 $-> a1)
   {b0 b1 : B} (g : b0 $-> b1)
@@ -81,6 +104,15 @@ Definition fmap11' {A B C : Type} `{IsGraph A, IsGraph B, Is01Cat C}
   : F a0 b0 $-> F a1 b1
   := fmap (flip F _) f $o fmap (F _) g.
 
+(** There are two ways to [fmap] in both arguments of a bifunctor. The bifunctor coherence condition ([bifunctor_isbifunctor]) states precisely that these two routes agree. *)
+Definition fmap11_coh {A B C : Type}
+  (F : A -> B -> C) `{Is1Bifunctor A B C F}
+  {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
+  : fmap11 F f g $== fmap11' F f g.
+Proof.
+  rapply bifunctor_isbifunctor. 
+Defined.
+
 Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} {f : a0 $-> a1} {f' : a0 $-> a1}
@@ -92,11 +124,8 @@ Definition fmap22 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
 Global Instance iemap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
   {a0 a1 : A} (f : a0 $<~> a1) {b0 b1 : B} (g : b0 $<~> b1)
-  : CatIsEquiv (fmap11 F f g).
-Proof.
-  rapply compose_catie'.
-  exact (iemap (flip F _) f).
-Defined.
+  : CatIsEquiv (fmap11 F f g)
+  := compose_catie' _ _.
 
 Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
   (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F}
@@ -104,6 +133,18 @@ Definition emap11 {A B C : Type} `{HasEquivs A, HasEquivs B, HasEquivs C}
   : F a0 b0 $<~> F a1 b1
   := Build_CatEquiv (fmap11 F f g).
 
+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)
+  : fmap10 F f b $== fmap11 F f (Id b)
+  := ((fmap_id _ _ $@R _) $@ cat_idl _)^$.
+
+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)
+  : fmap01 F a g $== fmap11 F (Id a) g
+  := ((_ $@L fmap_id _ _) $@ cat_idr _)^$.
+
 (** Any 0-bifunctor [A -> B -> C] can be made into a functor from the product category [A * B -> C] in two ways. *)
 Global Instance is0functor_uncurry_bifunctor {A B C : Type}
   `{IsGraph A, IsGraph B, Is01Cat C} (F : A -> B -> C) `{!Is0Bifunctor F}
diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index c3e6b80c442..bf37beb16be 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -2,7 +2,9 @@ Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall.
 Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv WildCat.NatTrans.
 
-(** * Monoidal 1-categories *)
+(** * Monoidal Categories *)
+
+(** In this file we define monoidal categories and symmetric monoidal categories. *)
 
 (** ** Typeclasses for common diagrams *)
 
@@ -65,7 +67,44 @@ Class PentagonIdentity {A : Type} `{HasEquivs A}
 Coercion pentagon_identity : PentagonIdentity >-> Funclass.
 Arguments pentagon_identity {A _ _ _ _ _} F {_ _ _} unit {_}.
 
-(** ** Definition *)
+(** *** Symmetors or Braiding *)
+
+Definition is0bifunctor_flip {A B C : Type}
+  (F : A -> B -> C) `{Is0Bifunctor A B C F} : Is0Bifunctor (flip F).
+Proof.
+  snrapply Build_Is0Bifunctor.
+  - exact _.
+  - exact _.
+Defined.
+
+Hint Immediate is0bifunctor_flip : typeclass_instances.
+
+Class Symmetor {A : Type} `{HasEquivs A}
+  (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} := {
+  (** An isomorphism [symmetor] witnessing the symmetry of [F]. *)
+  symmetor a b : F a b $<~> F b a;
+  (** The [symmetor] is a natural isomorphism. *)
+  is1natural_symmetor_uncurried
+    : Is1Natural
+      (uncurry F)
+      (uncurry (flip F))
+      (fun '(a, b) => symmetor a b);
+}.
+    
+Coercion symmetor : Symmetor >-> Funclass.
+Arguments symmetor {A _ _ _ _ _ F _ _ _} a b.
+
+(** *** Hexagon identity *)
+
+Class HexagonIdentity {A : Type} `{HasEquivs A}
+  (F : A -> A -> A)
+  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F, !Symmetor F}
+  (** The hexagon identity for an associator and symmetor. *)
+  := hexagon_identity a b c
+    : fmap10 F (symmetor b a) c $o associator b a c $o fmap01 F b (symmetor c a)
+      $== associator a b c $o symmetor (F b c) a $o associator b c a.
+
+(** ** Monoidal Categories *)
 
 (** A monoidal 1-category is a 1-category with equivalences together with the following: *)
 Class IsMonoidal (A : Type) `{HasEquivs A}
@@ -89,3 +128,202 @@ Class IsMonoidal (A : Type) `{HasEquivs A}
   (** The pentagon identity. *)
   cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor cat_tensor_unit;
 }.
+
+(** ** Symmetric Monoidal Categories *)
+
+(** A symmetric monoidal 1-category is a 1-category with equivalences together with the following: *)
+Class IsSymmetricMonoidal (A : Type) `{HasEquivs A}
+  (** A binary operation [cat_tensor] called the tensor product. *)
+  (cat_tensor : A -> A -> A)
+  (** A unit object [cat_tensor_unit] called the tensor unit. *)
+  (cat_tensor_unit : A)
+  := {
+  (** A monoidal structure with [cat_tensor] and [cat_tensor_unit]. *) 
+  issymmetricmonoidal_ismonoidal :: IsMonoidal A cat_tensor cat_tensor_unit;
+  (** A natural isomorphism [symmetor] witnessing the symmetry of the tensor product. *) 
+  cat_symm_tensor_symmetor :: Symmetor cat_tensor;
+  (** The hexagon identity. *)
+  cat_symm_tensor_hexagon :: HexagonIdentity cat_tensor;
+}.
+
+(** *** Building Symmetric Monoidal Categories *)
+
+Require Import Square.
+
+Section TwistConstruction.
+
+  Context (A : Type) `{HasEquivs A}
+    (cat_tensor : A -> A -> A) (cat_tensor_unit : A)
+    `{!Is0Bifunctor cat_tensor, !Is1Bifunctor cat_tensor}
+
+    (swap : forall a b, cat_tensor a b $-> cat_tensor b a)
+    (swap_swap : forall a b, swap a b $o swap b a $== Id _)
+    (swap_nat : forall a b c d (f : a $-> c) (g : b $-> d),
+      swap c d $o fmap11 cat_tensor f g
+      $== fmap11 cat_tensor g f $o swap a b)
+    
+    (twist : forall a b c, cat_tensor a (cat_tensor b c) $-> cat_tensor b (cat_tensor a c))
+    (twist_twist : forall a b c, twist a b c $o twist b a c $== Id _)
+    (twist_nat : forall a a' b b' c c' (f : a $-> a') (g : b $-> b') (h : c $-> c'),
+      twist a' b' c' $o fmap11 cat_tensor f (fmap11 cat_tensor g h)
+      $== fmap11 cat_tensor g (fmap11 cat_tensor f h) $o twist a b c)
+      
+    {left_unitor : LeftUnitor cat_tensor cat_tensor_unit}
+    {right_unitor : RightUnitor cat_tensor cat_tensor_unit}
+  
+    (swap_unitor : forall a, cate_fun (left_unitor a)
+      $== right_unitor a $o swap cat_tensor_unit a)
+    (twist_unitor : forall a b, fmap01 cat_tensor a (right_unitor b)
+      $== swap b a $o fmap01 cat_tensor b (right_unitor a) $o twist a b cat_tensor_unit)
+  
+    (twist_hexagon : forall a b c,
+      fmap01 cat_tensor c (swap b a) $o twist b c a $o fmap (cat_tensor b) (swap a c)
+      $== twist a c b $o fmap01 cat_tensor a (swap b c) $o twist b a c)
+  .
+
+  Local Definition swape a b
+    : cat_tensor a b $<~> cat_tensor b a
+    := cate_adjointify (swap a b) (swap b a) (swap_swap a b) (swap_swap b a).
+
+  Local Definition twiste a b c
+    : cat_tensor a (cat_tensor b c) $<~> cat_tensor b (cat_tensor a c)
+    := cate_adjointify (twist a b c) (twist b a c)
+        (twist_twist a b c) (twist_twist b a c).
+
+  Local Definition associator_twist' a b c
+    : cat_tensor a (cat_tensor b c) $<~> cat_tensor (cat_tensor a b) c.
+  Proof.
+    (** We can build the associator out of [swape] and [twiste]. *)
+    nrefine (swape _ _ $oE _).
+    nrefine (twiste _ _ _ $oE _).
+    exact (emap01 cat_tensor a (swape _ _)).
+    Show Proof.
+  Defined.
+
+  Local Definition associator_twist'_unfold a b c
+    : cate_fun (associator_twist' a b c)
+    $== swap c (cat_tensor a b) $o (twist a c b $o fmap01 cat_tensor a (swap b c)).
+  Proof.
+    refine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
+    nrefine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)).
+    refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+    apply cate_buildequiv_fun.
+  Defined.
+
+  Local Instance associator_twist : Associator cat_tensor.
+  Proof.
+    snrapply Build_Associator.
+    - exact associator_twist'.
+    - simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h.
+      (** To prove naturality it will be easier to reason about squares. *)
+      change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
+      (** First we remove all the equivalences from the equation. *)
+      nrapply hconcatL.
+      1: apply associator_twist'_unfold.
+      nrapply hconcatR.
+      2: apply associator_twist'_unfold.
+      (** The first square involving [swap] on its own is a naturality square. *)
+      nrapply vconcat.
+      2: apply swap_nat.
+      (** The second square is just the naturality of twist. *)
+      nrapply vconcat.
+      2: apply twist_nat.
+      (** We rewrite one of the edges to make sure a functor application is grouped together. *)
+      nrapply vconcatL.
+      { refine ((cat_assoc _ _ _)^$ $@ (_^$ $@R _)).
+        rapply fmap_comp. }
+      (** This allows us to compose with bifunctor coherence on one side. *) 
+      nrapply hconcat.
+      1: rapply fmap11_coh.
+      (** Leaving us with a square with a functor application. *) 
+      rapply fmap_square.
+      (** We are finally left with the naturality of swap. *)
+      apply swap_nat. 
+  Defined.
+
+  (** We can prove the triangle identity using two simpler coherences. The first is called [swap_unitor] and asserts that the the left unitor is the right unitor when composed with the [symmetor]. The second is called [twist_unitor] and asserts a reduced version of the triangle identity only mentioning [right_unitor], [swap] and [twist]. *)
+  Local Instance triangle_twist : TriangleIdentity cat_tensor cat_tensor_unit.
+  Proof.
+    intros a b.
+    refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
+    refine (_ $@ cat_assoc _ _ _).
+    nrapply cate_moveL_eM.
+    nrefine (_ $@L (emap_inv _ _ $@ cate_buildequiv_fun _) $@ _).
+    refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ _).
+    { apply cate_moveR_eV.
+      refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
+      apply swap_unitor. }
+    refine (_ $@ ((_ $@ (_ $@L (cate_buildequiv_fun _)^$)) $@R _)).
+    2: { refine (_ $@ ((fmap10_is_fmap11 _ _ _)^$ $@R _)).
+      apply swap_nat. }
+    refine (_ $@ (_^$ $@@ _)).
+    2: apply cate_buildequiv_fun.
+    2: refine (_ $@L fmap01_is_fmap11 _ _ _).
+    apply twist_unitor.
+  Defined.
+    
+  Local Instance pentagon_twist : PentagonIdentity cat_tensor cat_tensor_unit.
+  Proof.
+    hnf.
+    intros a b c d.
+    (** We probably want to unfold equivalences here but we might need to move them around, not quite sure. *)
+    (* refine ((_ $@@ _) $@ _ $@ (_ $@@ (_ $@R _))^$). *)
+  Admitted.
+  
+  Local Instance ismonoidal_twist
+    : IsMonoidal A cat_tensor cat_tensor_unit
+    := {}.
+
+  Local Instance symmetor_twist : Symmetor cat_tensor.
+  Proof.
+    snrapply Build_Symmetor.
+    - exact swape.
+    - intros [a b] [c d] [f g].
+      nrefine ((cate_buildequiv_fun _ $@R _) $@ _).
+      refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
+      nrefine (swap_nat _ _ _ _ _ _ $@ (_ $@R _)).
+      rapply bifunctor_isbifunctor.
+  Defined.
+
+  Local Instance hexagon_twist : HexagonIdentity cat_tensor.
+  Proof.
+    intros a b c.
+    refine (((_ $@L _) $@R _) $@ _ $@ (_ $@@ (_ $@R _))^$).
+    1,3,4: apply associator_twist'_unfold.
+    do 2 refine (((cat_assoc _ _ _)^$ $@R _) $@ _).
+    refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _).
+    { refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine (_ $@L cate_buildequiv_fun _ $@ _).
+      apply swap_swap. }
+    refine (cat_idr _ $@ _).
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)).
+    refine (_ $@ (((cat_idr _)^$ $@ (_ $@L _^$)) $@R _)).
+    2: { refine (cate_buildequiv_fun _ $@R _ $@ _).
+      apply swap_swap. }
+    nrefine ((_ $@R _) $@ _).
+    { refine ((_ $@R _) $@ _^$).
+      1: rapply fmap10_is_fmap11.
+      apply swap_nat. }
+    refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$).
+    refine (((fmap01_is_fmap11 _ _ _ $@ fmap22 _ (Id _) _^$)^$ $@R _) $@ _).
+    1: apply cate_buildequiv_fun.
+    refine (_ $@ cat_assoc _ _ _).
+    rapply (cate_epic_equiv (emap01 cat_tensor b (swape a c))).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L (_ $@ (_ $@L _^$)))).
+    3: exact (cate_buildequiv_fun _ $@ fmap2 _ (cate_buildequiv_fun _)).
+    2: refine ((fmap_id _ _)^$ $@ fmap2 _ (swap_swap _ _)^$ $@ fmap_comp _ _ _).
+    refine (_ $@ (cat_idr _)^$).
+    refine ((_ $@L _) $@ _).
+    1: exact (cate_buildequiv_fun _ $@ fmap2 _ (cate_buildequiv_fun _)).
+    apply twist_hexagon.
+  Defined.
+    
+  Local Instance issymmetricmonoidal_twist
+    : IsSymmetricMonoidal A cat_tensor cat_tensor_unit
+    := {}.
+
+End TwistConstruction.