{A : Type} `{HasBinaryProducts A} {w x y z : A} (f : w $-> y) (g : x $-> z) : cat_pr2 $o fmap11 (fun x y => cat_binprod x y) f g $== g $o cat_pr2 := cat_binprod_beta_pr2 _ _.
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