{z : A} (f : z $-> x) (g : z $-> y) : z $-> cat_binprod. Proof. nrapply (cat_prod_corec Bool). intros [|]. - exact f. - exact g. 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