a b {c c'} (h : c $-> c') : twist a b c' $o fmap01 cat_tensor a (fmap01 cat_tensor b h) $== fmap01 cat_tensor b (fmap01 cat_tensor a h) $o twist a b c. Proof. refine ((_ $@L _^$) $@ twist_nat a a b b c c' (Id _) (Id _) h $@ (_ $@R _)). - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _). rapply fmap01_is_fmap11. - refine (fmap12 _ _ _ $@ fmap01_is_fmap11 _ _ _). rapply fmap01_is_fmap11. 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.