{z : A} {f f' : forall i, z $-> x i} : (forall i, f i $== f' i) -> cat_prod_corec f $== cat_prod_corec f'. Proof. intros p. unfold cat_prod_corec. nrapply (moveL_equiv_V_0gpd cate_cat_prod_corec_inv). nrefine (cate_isretr cate_cat_prod_corec_inv _ $@ _). exact p. 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