NatEquiv (yon_0gpd (cat_prod I x)) (fun z : A^op => prod_0gpd I (fun i => yon_0gpd (x i) z)). Proof. snrapply Build_NatEquiv. 1: intro; nrapply cate_cat_prod_corec_inv. exact (is1natural_yoneda_0gpd (cat_prod I x) (fun z => prod_0gpd I (fun i => yon_0gpd (x i) z)) cat_pr). 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