{A : Type} `{hbp : HasBinaryProducts A} : HasBinaryCoproducts A^op := hbp.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans