From dce3174c952e3cdd35becdef3ce7715f0a685df0 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Thu, 9 Jan 2025 11:35:51 +0000
Subject: [PATCH] symmetric monoidal categories satisfy the other hexagon

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: 4b220fec-5da6-466f-82c3-c6949e3185e0 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/WildCat/Monoidal.v | 76 +++++++++++++++++++++++++------------
 1 file changed, 51 insertions(+), 25 deletions(-)

diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v
index 1e47b01c80..5440f3f331 100644
--- a/theories/WildCat/Monoidal.v
+++ b/theories/WildCat/Monoidal.v
@@ -113,8 +113,21 @@ Class HexagonIdentity {A : Type} `{HasEquivs A}
 Coercion hexagon_identity : HexagonIdentity >-> Funclass.
 Arguments hexagon_identity {A _ _ _ _ _} F {_ _}.
 
+(** *** Hexagon identity with inverse associators *)
+
 (** ** Monoidal Categories *)
 
+Class HexagonIdentityInverseAssoc {A : Type} `{HasEquivs A}
+  (F : A -> A -> A)
+  `{!Is0Bifunctor F, !Is1Bifunctor F, !Associator F, !Braiding F}
+  (** The other hexagon identity for an associator and a braiding. *)
+  := hexagon_identity_inv_assoc a b c
+  : fmap01 F b (braid a c) $o (associator b a c)^-1$ $o fmap10 F (braid a b) c
+      $== (associator b c a)^-1$ $o braid a (F b c) $o (associator a b c)^-1$. 
+
+Coercion hexagon_identity_inv_assoc : HexagonIdentityInverseAssoc >-> Funclass.
+Arguments hexagon_identity_inv_assoc {A _ _ _ _ _} F {_ _}.
+
 (** A monoidal 1-category is a 1-category with equivalences together with the following: *)
 Class IsMonoidal (A : Type) `{HasEquivs A}
   (** It has a binary operation [cat_tensor] called the tensor product. *)
@@ -439,6 +452,42 @@ Definition symmetricbraiding_op' {A : Type} {F : A -> A -> A}
     H' : !SymmetricBraiding (A:=A^op) F}
   : SymmetricBraiding F
   := symmetricbraiding_op (A:=A^op) (F := F).
+  
+(** Symmetric monoidal categories also satisfy the other hexagon axiom. This is very close to the hexagon axiom of the opposite monoidal category. *)
+Global Instance cat_symm_tensor_hexagon_inv_assoc
+  {A : Type} {F : A -> A -> A} {unit : A}
+  `{IsSymmetricMonoidal A F unit}
+  : HexagonIdentityInverseAssoc F.
+Proof.
+  intros a b c.
+  snrefine (_ $@ ((_ $@L _) $@R _)).
+  2: exact ((braide _ _)^-1$).
+  2: { nrapply cate_moveR_V1.
+    symmetry.
+    nrefine ((_ $@R _) $@ _).
+    1: nrapply cate_buildequiv_fun.
+    rapply braid_braid. }
+  nrefine (cat_assoc _ _ _ $@ _).
+  snrefine ((_ $@R _) $@ _).
+  { refine (emap _ _)^-1$.
+    rapply braide. }
+  { symmetry.
+    refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
+    nrapply cate_inv_adjointify. }
+  snrefine ((_ $@L (_ $@L _)) $@ _).
+  { refine (emap (flip F c) _)^-1$.
+    rapply braide. }
+  { symmetry.
+    refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
+    nrapply cate_inv_adjointify. }
+  nrefine (_ $@ cat_assoc_opp _ _ _).
+  refine ((_ $@L _)^$ $@ _^$ $@ cate_inv2 _ $@ _ $@ (_ $@L _)).
+  1,2,4,5: rapply cate_inv_compose'.
+  refine (_ $@ (_ $@@ _) $@ _ $@ (_ $@R _)^$ $@ _^$).
+  1-3,5-6: rapply cate_buildequiv_fun.
+  refine ((fmap02 _ _ _ $@@ ((_ $@ fmap20 _ _ _) $@R _)) $@ cat_symm_tensor_hexagon a b c $@ ((_ $@L _^$) $@R _)).
+  1-4: nrapply cate_buildequiv_fun.
+Defined.
 
 (** ** Opposite Monoidal Categories *)
 
@@ -479,31 +528,8 @@ Proof.
   - rapply ismonoidal_op.
   - rapply symmetricbraiding_op.
   - intros a b c; unfold op in a, b, c; simpl.
-    snrefine (_ $@ (_ $@L (_ $@R _))).
-    2: exact ((braide _ _)^-1$).
-    2: { nrapply cate_moveR_V1.
-      symmetry.
-      nrefine ((_ $@R _) $@ _).
-      1: nrapply cate_buildequiv_fun.
-      rapply braid_braid. }
-    snrefine ((_ $@R _) $@ _).
-    { refine (emap _ _)^-1$.
-      rapply braide. }
-    { symmetry.
-      refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
-      nrapply cate_inv_adjointify. }
-    snrefine ((_ $@L (_ $@L _)) $@ _).
-    { refine (emap (flip tensor c) _)^-1$.
-      rapply braide. }
-    { symmetry.
-      refine (cate_inv_adjointify _ _ _ _ $@ fmap2 _ _).
-      nrapply cate_inv_adjointify. }
-    refine ((_ $@L _)^$ $@ _^$ $@ cate_inv2 _ $@ _ $@ (_ $@L _)).
-    1,2,4,5: rapply cate_inv_compose'.
-    refine (_ $@ (_ $@@ _) $@ _ $@ (_ $@R _)^$ $@ _^$).
-    1-3,5-6: rapply cate_buildequiv_fun.
-    refine ((fmap02 _ _ _ $@@ ((_ $@ fmap20 _ _ _) $@R _)) $@ cat_symm_tensor_hexagon a b c $@ ((_ $@L _^$) $@R _)).
-    1-4: nrapply cate_buildequiv_fun.
+    nrefine (cat_assoc_opp _ _ _ $@ _ $@ cat_assoc _ _ _).
+    nrapply cat_symm_tensor_hexagon_inv_assoc.
 Defined.
 
 Definition issymmetricmonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A)