LeftUnitor cat_tensor cat_tensor_unit. Proof. snrapply Build_NatEquiv'. - snrapply Build_NatTrans. + exact (fun a => right_unitor a $o braid cat_tensor_unit a). + snrapply Build_Is1Natural. intros a b f. change (?w $o ?x $== ?y $o ?z) with (Square z w x y). nrapply vconcat. 2: rapply (isnat right_unitor f). rapply braid_nat_r. - intros a. rapply compose_catie'. rapply catie_braid. 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.