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