(x y : A) : cat_binprod x y $-> cat_binprod y x := cat_binprod_corec cat_pr2 cat_pr1.
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