{z : A} (f : z $-> cat_prod I x) : cat_prod_corec (fun i => cat_pr i $o f) $== f. Proof. exact (cate_issect 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