Merge pull request #2116 from Alizter/ps/rr/more_polymorphic_terminal…

…_unit_and_initial_empty more polymorphic terminal unit and initial empty
HoTT · Oct 13, 2024 · 8b9719e · 8b9719e
2 parents 6780b53 + e6d7256
commit 8b9719e
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).