diff --git a/theories/WildCat/Bifunctor.v b/theories/WildCat/Bifunctor.v
index f9cdaa63816..0929ea8c426 100644
--- a/theories/WildCat/Bifunctor.v
+++ b/theories/WildCat/Bifunctor.v
@@ -145,6 +145,14 @@ Definition fmap01_is_fmap11 {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
   : fmap01 F a g $== fmap11 F (Id a) g
   := ((_ $@L fmap_id _ _) $@ cat_idr _)^$.
 
+Definition fmap11_id {A B C : Type} `{Is1Cat A, Is1Cat B, Is1Cat C}
+  (F : A -> B -> C) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : A) (b : B)
+  : fmap11 F (Id a) (Id b) $== Id (F a b).
+Proof.
+  refine ((_ $@@ _) $@ cat_idr _).
+  1,2: rapply fmap_id.
+Defined.
+
 (** 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 bf37beb16be..5c6147e7a60 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -168,11 +168,7 @@ Section TwistConstruction.
       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)
+    (right_unitor : RightUnitor cat_tensor cat_tensor_unit)
     (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)
   
@@ -197,7 +193,6 @@ Section TwistConstruction.
     nrefine (swape _ _ $oE _).
     nrefine (twiste _ _ _ $oE _).
     exact (emap01 cat_tensor a (swape _ _)).
-    Show Proof.
   Defined.
 
   Local Definition associator_twist'_unfold a b c
@@ -241,7 +236,40 @@ Section TwistConstruction.
       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 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 left_unitor_twist : LeftUnitor cat_tensor cat_tensor_unit.
+  Proof.
+    snrapply Build_NatEquiv.
+    - exact (fun a => right_unitor a $oE swape cat_tensor_unit a).
+    - intros a b f.
+      change (?w $o ?x $== ?y $o ?z) with (Square z w x y).
+      nrapply hconcatL.
+      1: apply cate_buildequiv_fun.
+      nrapply hconcatR.
+      2: apply cate_buildequiv_fun.
+      nrapply vconcat.
+      2: rapply (isnat right_unitor f).
+      nrapply hconcatL.
+      1: apply cate_buildequiv_fun.
+      nrapply hconcatR.
+      2: apply cate_buildequiv_fun.
+      nrapply vconcatL.
+      1: rapply fmap01_is_fmap11.
+      nrapply vconcatR.
+      2: rapply fmap10_is_fmap11.
+      rapply swap_nat.
+  Defined.
+    
   Local Instance triangle_twist : TriangleIdentity cat_tensor cat_tensor_unit.
   Proof.
     intros a b.
@@ -253,8 +281,7 @@ Section TwistConstruction.
     nrefine (_ $@L (emap_inv _ _ $@ cate_buildequiv_fun _) $@ _).
     refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ _).
     { apply cate_moveR_eV.
-      refine (_ $@ (_ $@L (cate_buildequiv_fun _)^$)).
-      apply swap_unitor. }
+      apply cate_buildequiv_fun. }
     refine (_ $@ ((_ $@ (_ $@L (cate_buildequiv_fun _)^$)) $@R _)).
     2: { refine (_ $@ ((fmap10_is_fmap11 _ _ _)^$ $@R _)).
       apply swap_nat. }
@@ -268,25 +295,161 @@ Section TwistConstruction.
   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 _))^$). *)
+
+    Infix "⊗" := cat_tensor (at level 40).
+    Infix "⊗R" := (fmap01 cat_tensor) (at level 40).
+    Infix "⊗L" := (fmap10 cat_tensor) (at level 40).
+    Notation σ := swap.
+    Notation τ := twist.
+    Notation α := associator_twist.
+    Notation "f ∘ g" := (f $o g) (at level 60).
+
+    refine (_ $@ (_^$ $@R _)). 
+    2: { refine ((_ $@L associator_twist'_unfold _ _ _) $@ _).
+      refine ((cat_assoc _ _ _)^$ $@ _).
+      refine (_ $@R _).
+      refine ((_ $@R _) $@ _^$).
+      1: rapply fmap10_is_fmap11.
+      refine (_ $@ _).
+      2: apply swap_nat.
+      refine (_ $@L _).
+      rapply fmap01_is_fmap11. }
+    
+    refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)).
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    
+    refine ((_ $@R _) $@ _).
+    1: apply associator_twist'_unfold.
+    refine (cat_assoc _ _ _ $@ _).
+    refine (_ $@L _).
+
+    refine (_ $@ (_ $@L (fmap2 _ _ $@ _)^$)).
+    2: apply associator_twist'_unfold. 
+    2: rapply fmap_comp.
+
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ (_^$ $@R _)).
+    2: { refine (cat_assoc _ _ _ $@ (_ $@L _)).
+      refine (cat_assoc _ _ _ $@ _).
+      refine ((_ $@L _) $@ cat_idr _).
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      apply swap_swap. }
+    
+    refine ((_ $@L _) $@ _).
+    1: apply associator_twist'_unfold.
+
+    refine (_ $@ (_ $@L _^$)).
+    2: rapply fmap_comp.
+
+    change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).
+
+    refine (_ $@ cat_assoc _ _ _).
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    refine ((cat_assoc _ _ _)^$ $@ _).
+    
+    (** Now we move the first (right-most) symmetry on the RHS to the left. *)
+    apply (cate_epic_equiv (emap01 cat_tensor a (emap01 cat_tensor b (swape d c)))).
+    (** Cancelling on the right. *) 
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (cat_idr _)^$ $@ (_ $@L _^$)).
+    2: { refine ((_ $@L _) $@ _).
+      { refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+        refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+        apply cate_buildequiv_fun. }
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      apply swap_swap. }
+    
+    refine ((_ $@L _) $@ _).
+    { refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+      refine (cate_buildequiv_fun _ $@ fmap2 _ _).
+      apply cate_buildequiv_fun. }
+
+    do 2 change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g). 
+    
+    refine (cat_assoc _ _ _ $@ _).
+    refine ((_ $@L _) $@ _).
+    { refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _).
+      refine ((_ $@L _) $@ _).
+      1: rapply fmap01_is_fmap11.
+      refine (_ $@ _).
+      1: apply swap_nat.
+      refine (_^$ $@R _).
+      rapply fmap10_is_fmap11. }
+    refine ((_ $@L _) $@ _).
+    1: rapply fmap_comp.
+
+    change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).
+    refine ((cat_assoc _ _ _)^$ $@ (_ $@R _) $@ _).
+    { refine (cat_assoc _ _ _ $@ (_ $@L _)).
+      refine ((_ $@L _) $@ twist_nat _ _ _ _ _ _ _ _ _).  
+      refine (fmap2 _ _ $@ fmap01_is_fmap11 _ _ _).
+      refine (fmap10_is_fmap11 _ _ _). }
+    refine (((_ $@L (_^$ $@R _)) $@R _) $@ _).
+    { refine (_ $@ fmap22 _ (Id _) _^$). 
+      2: rapply fmap11_id.
+      rapply fmap10_is_fmap11. }
+    
+    (** Moving a swap inwards and cancelling. *)
+    refine ((_ $@R _) $@ _).
+    { refine ((cat_assoc _ _ _)^$ $@ _).
+      refine (_ $@R _).
+      refine ((cat_assoc _ _ _) $@ _).
+      refine ((_ $@L _) $@ _).
+      { refine ((_ $@L _) $@ _).
+        1: rapply fmap10_is_fmap11.
+        refine (_ $@ _).
+        1: nrapply swap_nat.
+        refine (_^$ $@R _).
+        rapply fmap01_is_fmap11. }
+      refine ((cat_assoc _ _ _)^$ $@ (_ $@R _)).
+      refine (cat_assoc _ _ _ $@ _).
+      refine ((_ $@L _) $@ cat_idr _).
+      refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _).
+      rapply swap_swap. }
+    
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    
+    refine (_ $@ (_^$ $@R _)). 
+    2: { refine (fmap2 _ _ $@ _).
+      1: apply associator_twist'_unfold.
+      refine (fmap_comp _ _ _ $@ _).
+      refine (_ $@L _).
+      refine (fmap_comp _ _ _). }
+    change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).
+
+    refine (_ $@ (cat_assoc _ _ _)^$).
+    refine (_ $@ (_ $@L _)).
+    2: { refine ((_ $@L _) $@ (cat_assoc _ _ _)^$).
+      refine (_ $@ cat_assoc _ _ _).
+      refine (_ $@ (_ $@R _)).
+      2: { refine (_ $@ (_^$ $@R _)).
+        2: { refine (fmap01_is_fmap11 _ _ _ $@ fmap22 _ (Id _) _).
+          rapply fmap01_is_fmap11. }
+        apply twist_nat. }
+      refine ((_ $@L _) $@R _).
+      refine (fmap2 _ _ $@ fmap01_is_fmap11 _ _ _).
+      rapply fmap01_is_fmap11. }
+    change (fmap (cat_tensor ?x) ?g) with (fmap01 cat_tensor x g).
+    
+    refine (_ $@ (_ $@L (_ $@L _))).
+    2: refine (cat_assoc _ _ _)^$.
+    refine (_ $@ cat_assoc _ _ _).
+    refine (_ $@ cat_assoc _ _ _).
+
+    (** Goal looks like:
+
+    ((τ (a ⊗ b) d c ∘ σ (d ⊗ c) (a ⊗ b)) ∘ τ a (d ⊗ c) b) ∘ a ⊗R σ b (d ⊗ c) $==
+((d ⊗R σ c (a ⊗ b) ∘ d ⊗R τ a c b) ∘ τ a d (c ⊗ b)) ∘ (a ⊗R (d ⊗R σ b c) ∘ a ⊗R τ b d c)
+
+    Not sure if we can simplify any further with naturality. I'm looking for a way to compose something to get this goal out of simpler pieces. If nothing can be found then this might just be the pentagon analgoue of twist. *)
+    
   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.