(x y : A) : cat_binprod_swap x y $o cat_binprod_swap y x $== Id _. Proof. nrapply cat_binprod_eta_pr. - refine ((cat_assoc _ _ _)^$ $@ _). nrefine (cat_binprod_beta_pr1 _ _ $@R _ $@ _). exact (cat_binprod_beta_pr2 _ _ $@ (cat_idr _)^$). - refine ((cat_assoc _ _ _)^$ $@ _). nrefine (cat_binprod_beta_pr2 _ _ $@R _ $@ _). exact (cat_binprod_beta_pr1 _ _ $@ (cat_idr _)^$). 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