{x x' y y' z z'} (f : x $-> x') (g : y $-> y') (h : z $-> z') : associator x' y' z' $o fmap11 F f (fmap11 F g h) $== fmap11 F (fmap11 F f g) h $o associator x y z. Proof. destruct assoc as [asso nat]. exact (nat (x, y, z) (x', y', z') (f, g, h)). 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.