{a b c d} (f : a $-> c) (g : b $-> d) : braid c d $o fmap11 F f g $== fmap11 F g f $o braid a b. Proof. exact (isnat braid_uncurried (a := (a, b)) (a' := (c, d)) (f, g)). 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.