Associator cat_tensor. Proof. snrapply Build_Associator. - exact '. - snrapply Build_Is1Natural. simpl; intros [[a b] c] [[a' b'] c'] [[f g] h]; simpl in f, g, h. change (?w $o ?x $== ?y $o ?z) with (Square z w x y). nrapply hconcatL. 1: apply '_unfold. nrapply hconcatR. 2: apply '_unfold. nrapply vconcat. 2: rapply braid_nat. nrapply vconcat. 2: apply twist_nat. nrapply hconcatL. 2: nrapply hconcatR. 1,3: symmetry; rapply fmap01_is_fmap11. rapply fmap11_square. 1: rapply vrefl. apply braid_nat. 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.