{A : Type} `{HasBinaryProducts A} {w x y z : A} (f g : w $-> cat_binprod x (cat_binprod y z)) : cat_pr1 $o f $== cat_pr1 $o g -> cat_pr1 $o cat_pr2 $o f $== cat_pr1 $o cat_pr2 $o g -> cat_pr2 $o cat_pr2 $o f $== cat_pr2 $o cat_pr2 $o g -> f $== g. Proof. intros p q r. snrapply cat_binprod_eta_pr. - exact p. - snrapply cat_binprod_eta_pr. + exact (cat_assoc_opp _ _ _ $@ q $@ cat_assoc _ _ _). + exact (cat_assoc_opp _ _ _ $@ r $@ cat_assoc _ _ _). 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