{I : Type} {A : Type} (x : A) `{Product I _ (fun _ => x)} : x $-> cat_prod I (fun _ => x) := cat_prod_corec I (fun _ => Id x).
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