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