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