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