{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 y y' : A} (g : y $-> y') : fmap_tensor F (x, y') $o fmap01 tensorB (F x) (fmap F g) $== fmap F (fmap01 tensorA x g) $o fmap_tensor F (x, y). Proof. refine ((_ $@L (fmap21 tensorB (fmap_id _ _) _ $@ fmap01_is_fmap11 _ _ _)^$) $@ _). refine (_ $@ (fmap2 F (fmap01_is_fmap11 _ _ _) $@R _)). snrapply fmap_tensor_nat. 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.