twist_hex' a b c d : fmap01 cat_tensor c (twist a b d) $o twist a c (cat_tensor b d) $o fmap01 cat_tensor a (twist b c d) $== twist b c (cat_tensor a d) $o fmap01 cat_tensor b (twist a c d) $o twist a b (cat_tensor c d). Proof. pose proof (twist_hexagon c a d $@ cat_assoc _ _ _) as p. apply moveR_twistL in p. apply moveR_fmap01_braidL in p. apply (fmap02 cat_tensor b) in p. refine (_ $@ ((_ $@L p) $@R _)); clear p. apply moveL_twistR. apply moveL_twistL. refine (_ $@ (fmap01_comp _ _ _ _)^$). apply moveR_twistL. refine (_ $@ cat_assoc _ _ _). Abort. End TwistConstruction.
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.