Merge pull request #2013 from Alizter/ps/rr/opposite_monoidal_categories

opposite monoidal categories

Author: Alizter

test/WildCat/Opposite.v

@@ -68,5 +68,5 @@ Fail Definition test A `{HasEquivs A}
 (** Opposite braidings are definitionally involutive. *)
 Succeed Definition test A `{HasEquivs A}
   (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Braiding F)
-  : @braiding_op _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ a) = a
+  : @braiding_op _ _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ _ a) = a
   := 1.

theories/WildCat/Monoidal.v

@@ -124,8 +124,8 @@ Class IsMonoidal (A : Type) `{HasEquivs A}
   (** These all satisfy the following properties: *)
   := {
   (** A [cat_tensor] is a 1-bifunctor. *)
-  is0bifunctor_cat_tensor :: Is0Bifunctor cat_tensor;
-  is1bifunctor_cat_tensor :: Is1Bifunctor cat_tensor;
+  is0bifunctor_cat_tensor : Is0Bifunctor cat_tensor;
+  is1bifunctor_cat_tensor : Is1Bifunctor cat_tensor;
   (** A natural isomorphism [associator] witnessing the associativity of the tensor product. *)
   cat_tensor_associator :: Associator cat_tensor;
   (** A natural isomorphism [left_unitor] witnessing the left unit law. *)
@@ -138,6 +138,9 @@ Class IsMonoidal (A : Type) `{HasEquivs A}
   cat_tensor_pentagon_identity :: PentagonIdentity cat_tensor;
 }.
 
+Existing Instance is0bifunctor_cat_tensor | 10.
+Existing Instance is1bifunctor_cat_tensor | 10.
+
 (** TODO: Braided monoidal categories *)
 
 (** ** Symmetric Monoidal Categories *)
@@ -207,6 +210,11 @@ Section Associator.
 
 End Associator.
 
+Definition associator_op' {A : Type} `{HasEquivs A} {F : A -> A -> A}
+  `{!Is0Bifunctor F, !Is1Bifunctor F, assoc : !Associator (A:=A^op) F}
+  : Associator F
+  := associator_op (A:=A^op) (assoc := assoc).
+
 (** ** Theory about [LeftUnitor] and [RightUnitor] *)
 
 Section LeftUnitor.
@@ -223,14 +231,15 @@ End LeftUnitor.
 
 (** ** Theory about [Braiding] *)
 
-Section Braiding.
-  Context {A : Type} `{HasEquivs A} {F : A -> A -> A}
-    `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F}.
-  
-  Global Instance braiding_op : Braiding (A:=A^op) F
-    := (nattrans_op (nattrans_flip braid)).
+Global Instance braiding_op {A : Type} `{HasEquivs A} {F : A -> A -> A}
+  `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding F}
+  : Braiding (A:=A^op) F
+  := nattrans_op (nattrans_flip braid).
 
-End Braiding.
+Definition braiding_op' {A : Type} `{HasEquivs A} {F : A -> A -> A}
+  `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding (A:=A^op) F}
+  : Braiding F
+  := braiding_op (A:=A^op) (braid := braid).
 
 (** ** Theory about [SymmetricBraid] *)
 
@@ -425,6 +434,12 @@ Section SymmetricBraid.
 
 End SymmetricBraid.
 
+Definition symmetricbraiding_op' {A : Type} {F : A -> A -> A}
+  `{HasEquivs A, !Is0Bifunctor F, !Is1Bifunctor F,
+    H' : !SymmetricBraiding (A:=A^op) F}
+  : SymmetricBraiding F
+  := symmetricbraiding_op (A:=A^op) (F := F).
+
 (** ** Opposite Monoidal Categories *)
 
 Global Instance ismonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A)
@@ -451,8 +466,52 @@ Proof.
     rapply cat_tensor_pentagon_identity.
 Defined.
 
-(** ** Further Coherence Conditions *)
+Definition ismonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A)
+  `{HasEquivs A} `{!IsMonoidal A^op tensor unit}
+  : IsMonoidal A tensor unit
+  := ismonoidal_op (A:=A^op) tensor unit.
 
+Global Instance issymmetricmonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A)
+  `{IsSymmetricMonoidal A tensor unit}
+  : IsSymmetricMonoidal A^op tensor unit.
+Proof.
+  snrapply Build_IsSymmetricMonoidal.
+  - 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.
+Defined.
+
+Definition issymmetricmonoidal_op' {A : Type} (tensor : A -> A -> A) (unit : A)
+  `{HasEquivs A} `{H' : !IsSymmetricMonoidal A^op tensor unit}
+  : IsSymmetricMonoidal A tensor unit
+  := issymmetricmonoidal_op (A:=A^op) tensor unit.
+
+(** ** Further Coherence Conditions *)
 (** In MacLane's original axiomatisation of a monoidal category, 3 extra coherence conditions were given in addition to the pentagon and triangle identities. It was later shown by Kelly that these axioms are redundant and follow from the rest. We reproduce these arguments here. *)
 
 (** The left unitor of a tensor can be decomposed as an associator and a functorial action of the tensor on a left unitor. *)