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