a b c d e f (g : e $-> _) : fmap01 cat_tensor a (twist b c d) $o f $== g -> f $== fmap01 cat_tensor a (twist c b d) $o g. Proof. intros p. apply (cate_monic_equiv (emap01 cat_tensor a (twiste b c d))). refine (_ $@ cat_assoc _ _ _). refine (_ $@ (_ $@R _)). 2: { refine (_ $@ (_^$ $@R _)). 2: apply cate_buildequiv_fun. refine ((fmap_id _ _)^$ $@ fmap2 _ _ $@ fmap_comp _ _ _). refine (_^$ $@ (_^$ $@R _)). 2: apply cate_buildequiv_fun. apply twist_twist. } refine ((_ $@R _) $@ p $@ (cat_idl _)^$). refine (cate_buildequiv_fun _ $@ fmap02 _ _ _). apply cate_buildequiv_fun. 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.