PentagonIdentity cat_tensor. Proof. clear twist_unitor right_unitor cat_tensor_unit. intros a b c d. refine ((_ $@@ _) $@ _ $@ ((fmap02 _ _ _ $@ _)^$ $@@ (_ $@@ (fmap20 _ _ _ $@ _))^$)). 1,2,4,6,7: apply associator_twist'_unfold. 2: refine (fmap01_comp _ _ _ _ $@ (_ $@L (fmap01_comp _ _ _ _))). 2: refine (fmap10_comp _ _ _ _ $@ (_ $@L (fmap10_comp _ _ _ _))). refine (cat_assoc _ _ _ $@ _). refine (_ $@L (cat_assoc _ _ _) $@ _). do 4 refine ((cat_assoc _ _ _)^$ $@ _). refine (_ $@ (((cat_assoc _ _ _) $@R _) $@R _)). do 2 refine (_ $@ ((cat_assoc _ _ _) $@R _)). do 2 refine (_ $@ cat_assoc _ _ _). apply moveL_fmap01_fmap01_braidR. apply moveL_fmap01_twistR. refine (_ $@ (cat_assoc _ _ _)^$). refine (_ $@ ((_ $@L _) $@ cat_idr _)^$). 2: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _). 2: apply braid_braid. apply moveL_twistR. refine (_ $@ (cat_assoc _ _ _)^$). refine (_ $@ (_ $@L _)). 2: apply braid_nat_r. refine (_ $@ cat_assoc _ _ _). apply moveL_fmap01_fmap01_braidR. refine (_ $@ (cat_assoc _ _ _)^$). refine (_ $@ (_ $@L _)). 2: apply braid_nat_r. refine (_ $@ cat_assoc _ _ _). apply moveL_fmap01_twistR. refine (_ $@ _). 2: apply braid_nat_r. apply moveR_fmap01_twistR. apply moveR_fmap01_fmap01_braidR. apply moveR_twistR. apply moveR_fmap01_twistR. refine (cat_assoc _ _ _ $@ _). refine ((_ $@L _) $@ _). 1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_comp _ _ _ _). 1: apply braid_nat_r. refine ((cat_assoc _ _ _)^$ $@ _). apply moveR_fmap01_braidR. refine (cat_assoc _ _ _ $@ _). refine ((_ $@L _) $@ _). 1: apply twist_nat_m. refine ((cat_assoc _ _ _)^$ $@ _). apply moveR_twistR. refine (cat_assoc _ _ _ $@ _). refine ((_ $@L _) $@ _). 1: apply braid_nat_l. refine ((cat_assoc _ _ _)^$ $@ _). apply moveR_braidR. refine (cat_assoc _ _ _ $@ _). refine ((_ $@L _) $@ cat_idr _ $@ _). 1: refine ((fmap01_comp _ _ _ _)^$ $@ fmap02 _ _ _ $@ fmap01_id _ _ _). 1: apply braid_braid. apply moveL_braidR. apply moveL_twistR. apply moveL_fmap01_braidR. do 4 refine (_ $@ (cat_assoc _ _ _)^$). do 3 refine (cat_assoc _ _ _ $@ _). refine (_ $@L _). apply moveR_twistL. do 4 refine (_ $@ cat_assoc _ _ _). refine ((cat_assoc _ _ _)^$ $@ _). apply moveL_fmap01_twistR. apply moveL_twistR. do 2 refine (_ $@ (cat_assoc _ _ _)^$). do 3 refine (cat_assoc _ _ _ $@ _). apply moveL_twistL. refine (_ $@ cat_assoc _ _ _). do 4 refine ((cat_assoc _ _ _)^$ $@ _). apply moveR_twistR. apply moveR_fmap01_twistR. do 3 refine (_ $@ (cat_assoc _ _ _)^$). do 2 refine (cat_assoc _ _ _ $@ _). apply moveL_fmap01_braidL. do 2 refine (_ $@ cat_assoc _ _ _). do 3 refine ((cat_assoc _ _ _)^$ $@ _). apply twist_9_gon. 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.