{a b c} (f : a $-> b) : braid b c $o fmap10 F f c $== fmap01 F c f $o braid a c. Proof. refine ((_ $@L (fmap10_is_fmap11 _ _ _)^$) $@ _ $@ (fmap01_is_fmap11 _ _ _ $@R _)). exact (isnat braid_uncurried (a := (a, c)) (a' := (b, c)) (f, Id _)). 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.