{I A : Type} `{HasEquivs A} (x : I -> A) `{!Product I x} (y : I -> A) `{!Product I y} (e : forall i : I, x i $<~> y i) : cat_prod I x $<~> cat_prod I y. Proof. exact (cate_cat_prod 1 x y e). 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