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.
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.