TriangleIdentity cat_tensor cat_tensor_unit. Proof. intros a b. refine (_ $@ (_ $@L _)^$). 2: apply associator_twist'_unfold. refine (fmap02 _ a (cate_buildequiv_fun _) $@ _); cbn. refine (fmap01_comp _ _ _ _ $@ _). do 2 refine (_ $@ cat_assoc _ _ _). refine ((twist_unitor _ _ $@ (_ $@R _)) $@R _). apply braid_nat_r. 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.