{A B : Type} {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B} (F : A -> B) `{IsMonoidalFunctor A B tensorA tensorB IA IB F} {x x' y y': A} (f : x $-> x') (g : y $-> y') : fmap_tensor F (x', y') $o fmap11 tensorB (fmap F f) (fmap F g) $== fmap F (fmap11 tensorA f g) $o fmap_tensor F (x, y). Proof. destruct (fmap_tensor F) as [fmap_tensor_F nat]. exact (nat (x, y) (x', y') (f, g)). 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.