{A : Type} `{Is1Cat A, !IsPointedCat A} (x y : A) `{!BinaryCoproduct x y, !BinaryProduct x y} : cat_bincoprod x y $-> cat_binprod x y. Proof. nrapply cat_coprod_prod; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans