{A : Type} `{Is1Cat A} {x y : A} `{!BinaryCoproduct x y} : y $-> cat_bincoprod x y := cat_pr2 (A:=A^op) (x:=x) (y:=y).
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans