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