{A : Type} `{Is1Cat A} (x : A) `{!BinaryCoproduct x x} : cat_bincoprod x x $-> x := cat_binprod_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