{z : A} (f f' : z $-> x) (g g' : z $-> y) : f $== f' -> g $== g' -> cat_binprod_corec f g $== cat_binprod_corec f' g'. Proof. intros p q. rapply cat_prod_corec_eta. intros [|]. - exact p. - exact q. 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