{a b c d : A} (f : a $-> c) (g : b $-> d) : cat_binprod_swap c d $o fmap11 (fun x y : A => cat_binprod x y) f g $== fmap11 (fun x y : A => cat_binprod x y) g f $o cat_binprod_swap a b := cat_binprod_swap_corec _ _ $@ (cat_binprod_fmap11_corec _ _ _ _)^$. Local Instance symmetricbraiding_binprod : SymmetricBraiding (fun x y => cat_binprod x y). Proof. snrapply Build_SymmetricBraiding. - snrapply Build_NatTrans. + intros [x y]. exact (cat_binprod_swap x y). + snrapply Build_Is1Natural. intros [a b] [c d] [f g]; cbn in f, g. exact( f g). - exact cat_binprod_swap_cat_binprod_swap. Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd