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