a b c : cate_fun (associator_twist' a b c) $== braid c (cat_tensor a b) $o (twist a c b $o fmap01 cat_tensor a (braid b c)). Proof. refine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)). nrefine (cate_buildequiv_fun _ $@ (_ $@@ cate_buildequiv_fun _)). refine (cate_buildequiv_fun _ $@ fmap2 _ _). 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.