(I : Type) {A : Type} `{Is1Cat A} {x : I -> A} (cat_coprod : A) (cat_in : forall i : I, x i $-> cat_coprod) (cat_coprod_rec : forall z : A, (forall i : I, x i $-> z) -> (cat_coprod $-> z)) (cat_coprod_beta_in : forall (z : A) (f : forall i, x i $-> z) (i : I), cat_coprod_rec z f $o cat_in i $== f i) (cat_prod_eta_in : forall (z : A) (f g : cat_coprod $-> z), (forall i : I, f $o cat_in i $== g $o cat_in i) -> f $== g) : Coproduct I x := Build_Product I (cat_coprod : A^op) cat_in cat_coprod_rec cat_coprod_beta_in cat_prod_eta_in.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans