(x y : A) {z z' : A} (h : z $-> z') : associator x y z' $o fmap01 F x (fmap01 F y h) $== fmap01 F (F x y) h $o associator x y z. Proof. refine ((_ $@L _^$) $@ _ $@ (_ $@R _)). 2: nrapply (associator_nat (Id _) (Id _) h). - exact (fmap12 _ _ (fmap01_is_fmap11 _ _ _) $@ fmap01_is_fmap11 _ _ _). - exact (fmap21 _ (fmap11_id _ _ _) _ $@ fmap01_is_fmap11 F _ _). 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.