{z : A} (f : forall i, z $-> x i) : forall i, cat_pr i $o cat_prod_corec f $== f i. Proof. exact (cate_isretr cate_cat_prod_corec_inv f). 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