{z : A} {f f' : z $-> cat_prod I x} : (forall i, cat_pr i $o f $== cat_pr i $o f') -> f $== f'. Proof. intros p. refine ((cat_prod_eta _)^$ $@ _ $@ cat_prod_eta _). by nrapply cat_prod_corec_eta. 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