a b c d e f (g : _ $-> e) : f $== g $o fmap01 F a (fmap01 F b (braid d c)) -> f $o fmap01 F a (fmap01 F b (braid c d)) $== g. Proof. intros p; symmetry; apply moveL_fmap01_fmap01_braidR; symmetry; exact p. 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.