From 27b6fc1d0ba6a6388a7413036eca95d522202632 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 4 Jul 2024 14:57:36 +0200 Subject: [PATCH 1/3] opposite monoidal categories Signed-off-by: Ali Caglayan --- theories/WildCat/Monoidal.v | 79 ++++++++++++++++++++++++++++++++----- 1 file changed, 69 insertions(+), 10 deletions(-) diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index bdbbce2df1d..bfa33c597b6 100644 --- a/theories/WildCat/Monoidal.v +++ b/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. *) From 8730d51d4e5838baa7d3d4537e8085eeb51467ab Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 4 Jul 2024 16:53:03 +0200 Subject: [PATCH 2/3] Update theories/WildCat/Monoidal.v Co-authored-by: Dan Christensen --- theories/WildCat/Monoidal.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/WildCat/Monoidal.v b/theories/WildCat/Monoidal.v index bfa33c597b6..188cb90b53a 100644 --- a/theories/WildCat/Monoidal.v +++ b/theories/WildCat/Monoidal.v @@ -234,7 +234,7 @@ End LeftUnitor. 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)). + := nattrans_op (nattrans_flip braid). Definition braiding_op' {A : Type} `{HasEquivs A} {F : A -> A -> A} `{!Is0Bifunctor F, !Is1Bifunctor F, braid : !Braiding (A:=A^op) F} From 4c82e003cb6217c1f0d71f2bbd0e6f48e6714d7b Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 4 Jul 2024 17:00:51 +0200 Subject: [PATCH 3/3] fix test Signed-off-by: Ali Caglayan --- test/WildCat/Opposite.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v index 65a5558b3fb..38d7aa0f157 100644 --- a/test/WildCat/Opposite.v +++ b/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.