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). Global Instance ismonoidal_op {A : Type} (tensor : A -> A -> A) (unit : A) `{IsMonoidal A tensor unit} : IsMonoidal A^op tensor unit. Proof. snrapply Build_IsMonoidal. 1-5: exact _. - intros a b; unfold op in a, b; simpl. refine (_^$ $@ _ $@ (_ $@L _)). 1,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _). nrefine (cate_inv2 _ $@ cate_inv_compose' _ _). refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _) $@ (cate_buildequiv_fun _)^$). rapply cat_tensor_triangle_identity. - intros a b c d; unfold op in a, b, c, d; simpl. refine (_ $@ ((_ $@L _) $@@ _)). 2,3: exact (emap_inv _ _ $@ cate_buildequiv_fun _). refine ((cate_inv_compose' _ _)^$ $@ cate_inv2 _ $@ cate_inv_compose' _ _ $@ (_ $@L cate_inv_compose' _ _)). refine (cate_buildequiv_fun _ $@ _ $@ ((cate_buildequiv_fun _)^$ $@R _) $@ (cate_buildequiv_fun _)^$). refine (_ $@ (cate_buildequiv_fun _ $@@ (cate_buildequiv_fun _ $@R _))^$). rapply cat_tensor_pentagon_identity. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.