{A : Type} `{Is1Cat A} {F : A -> A -> A} `{!Is0Bifunctor F, !Is1Bifunctor F, !Braiding F} : forall a b, F a b $-> F b a := fun a b => braid_uncurried (a, b).
Require Import Basics.Overture Basics.Tactics Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Opposite.