{I A : Type} `{Is1Cat A} (prod : A) (x : I -> A) (z : A) (pr : forall i, prod $-> x i) : yon_0gpd prod z $-> prod_0gpd I (fun i => yon_0gpd (x i) z). Proof. snrapply equiv_prod_0gpd_corec. intros i. exact (fmap (fun x => yon_0gpd x z) (pr i)). 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