(x y z : A) : cat_pr1 $o cat_binprod_twist x y z $== cat_pr1 $o cat_pr2 := cat_binprod_beta_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