From e6d72564ab81f982b38e2bf4ea82da6a14eeb486 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 10 Oct 2024 11:50:14 +0100 Subject: [PATCH] more polymorphic terminal unit and initial empty Signed-off-by: Ali Caglayan --- theories/WildCat/Universe.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v index 8926c3924a0..cf7aee45984 100644 --- a/theories/WildCat/Universe.v +++ b/theories/WildCat/Universe.v @@ -83,7 +83,7 @@ Defined. #[export] Hint Immediate catie_isequiv : typeclass_instances. -Global Instance isinitial_zero : IsInitial Empty. +Global Instance isinitial_zero : IsInitial (A:=Type) Empty. Proof. intro A. exists (Empty_rec _). @@ -91,7 +91,7 @@ Proof. rapply Empty_ind. Defined. -Global Instance isterminal_unit : IsTerminal Unit. +Global Instance isterminal_unit : IsTerminal (A:=Type) Unit. Proof. intros A. exists (fun _ => tt).