(x y z : A) : cat_binprod x (cat_binprod y z) $-> cat_binprod y (cat_binprod x z). Proof. nrapply cat_binprod_corec. - exact (cat_pr1 $o cat_pr2). - exact (fmap01 (fun x y => cat_binprod x y) x cat_pr2). 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