{A : Type} `{HasBinaryProducts A} {x y z : A} (f : cat_binprod x (cat_binprod y z) $-> cat_binprod x (cat_binprod y z)) : cat_pr1 $o f $== cat_pr1 -> cat_pr1 $o cat_pr2 $o f $== cat_pr1 $o cat_pr2 -> cat_pr2 $o cat_pr2 $o f $== cat_pr2 $o cat_pr2 -> f $== Id _. Proof. intros p q r. snrapply cat_binprod_eta_pr_x_xx. - exact (p $@ (cat_idr _)^$). - exact (q $@ (cat_idr _)^$). - exact (r $@ (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