{z : A} (f : z $-> cat_binprod) : cat_binprod_corec (cat_pr1 $o f) (cat_pr2 $o f) $== f. Proof. unfold cat_binprod_corec. nrapply cat_prod_pr_eta. intros [|]. - exact (cat_binprod_beta_pr1 _ _). - exact (cat_binprod_beta_pr2 _ _). 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