associator_twist' a b c : cat_tensor a (cat_tensor b c) $<~> cat_tensor (cat_tensor a b) c. Proof. refine (braide _ _ $oE _). nrefine (twiste _ _ _ $oE _). exact (emap01 cat_tensor a (braide _ _)). 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.