more polymorphic terminal unit and initial empty

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Oct 10, 2024 · e6d7256 · e6d7256
1 parent 9ed2b66
commit e6d7256
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/theories/WildCat/Universe.v b/theories/WildCat/Universe.v
@@ -83,15 +83,15 @@ 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 _).
   intros g.
   rapply Empty_ind.
 Defined.
 
-Global Instance isterminal_unit : IsTerminal Unit.
+Global Instance isterminal_unit : IsTerminal (A:=Type) Unit.
 Proof.
   intros A.
   exists (fun _ => tt).