{A : Type} {z : A} `{Coproduct Empty A (fun _ => z)} : IsInitial (cat_coprod Empty (fun _ => z)). Proof. intros a. snrefine (cat_coprod_rec _ _; fun f => cat_coprod_in_eta _ _); intros []. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Decidable. Require Import Types.Bool. Require Import WildCat.Core WildCat.Equiv WildCat.Forall WildCat.NatTrans