(x y z : A) : cat_binprod_twist x y z $o cat_binprod_twist y x z $== Id _. Proof. nrapply cat_binprod_eta_pr_x_xx_id. - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr1_twist _ _ _ $@R _) $@ _). nrapply cat_binprod_pr1_pr2_twist. - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr1_pr2_twist _ _ _ $@R _) $@ _). nrapply cat_binprod_pr1_twist. - nrefine (cat_assoc_opp _ _ _ $@ (cat_binprod_pr2_pr2_twist _ _ _ $@R _) $@ _). nrapply cat_binprod_pr2_pr2_twist. 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