{I : Type} {A : Type} (x : A) `{Coproduct I _ (fun _ => x)} : cat_coprod I (fun _ => x) $-> x := cat_prod_diag (A:=A^op) x.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans