HexagonIdentity cat_tensor. Proof. intros a b c; simpl. refine (((_ $@L _) $@R _) $@ _ $@ (_ $@@ (_ $@R _))^$). 1,3,4: apply associator_twist'_unfold. do 2 refine (((cat_assoc _ _ _)^$ $@R _) $@ _). refine (cat_assoc _ _ _ $@ (_ $@L _) $@ _). { refine ((fmap_comp _ _ _)^$ $@ fmap2 _ _ $@ fmap_id _ _). apply braid_braid. } refine (cat_idr _ $@ _). refine (_ $@ cat_assoc _ _ _). refine (_ $@ ((cat_assoc _ _ _)^$ $@R _)). refine (_ $@ (((cat_idr _)^$ $@ (_ $@L _^$)) $@R _)). 2: apply braid_braid. refine (((braid_nat_r _)^$ $@R _) $@ _). refine (cat_assoc _ _ _ $@ (_ $@L _) $@ (cat_assoc _ _ _)^$). refine (_ $@ cat_assoc _ _ _). apply moveL_fmap01_braidR. apply twist_hexagon. 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.