{A : Type} {z : A} `{Product Empty A (fun _ => z)} : IsTerminal (cat_prod Empty (fun _ => z)). Proof. intros a. snrefine (cat_prod_corec _ _; fun f => cat_prod_pr_eta _ _); intros []. Defined.
Require Import Basics.Equivalences Basics.Overture Basics.Tactics. Require Import Types.Bool Types.Prod Types.Forall. Require Import WildCat.Bifunctor WildCat.Core WildCat.Equiv WildCat.EquivGpd