{I J : Type} (ie : I <~> J) {A : Type} `{HasEquivs A} (x : I -> A) `{!Product I x} (y : J -> A) `{!Product J y} (e : forall i : I, x i $<~> y (ie i)) : cat_prod I x $<~> cat_prod J y. Proof. nrapply yon_equiv_0gpd. nrefine (natequiv_compose _ (natequiv_cat_prod_corec_inv _)). nrefine (natequiv_compose (natequiv_inverse (natequiv_cat_prod_corec_inv _)) _). snrapply Build_NatEquiv. - intros z. nrapply (cate_prod_0gpd ie). intros i. exact (natequiv_yon_equiv_0gpd (e i) _). - snrapply Build_Is1Natural. intros a b f g j. cbn. destruct (eisretr ie j). exact (cat_assoc_opp _ _ _). 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