a {b b'} (g : b $-> b') c : twist a b' c $o fmap01 cat_tensor a (fmap10 cat_tensor g c) $== fmap10 cat_tensor g (cat_tensor a c) $o twist a b c. Proof. refine ((_ $@L _^$) $@ twist_nat a a b b' c c (Id _) g (Id _) $@ (_ $@R _)). - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _). rapply fmap10_is_fmap11. - refine (fmap12 _ _ _ $@ fmap10_is_fmap11 _ _ _). rapply fmap11_id. Defined.
Require Import Basics.Overture Basics.Tactics Types.Forall WildCat.Monoidal. Require Import WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.Equiv. Require Import WildCat.NatTrans WildCat.Square WildCat.Opposite.