Free up universe in proofs of IsHSet, Decidable and DecidablePaths

jdchristensen · Jan 16, 2024 · a53efef · a53efef
1 parent 4a0c7b6
commit a53efef
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
@@ -34,15 +34,15 @@ Fixpoint fin_to_nat {n} : Fin n -> nat
          end
      end.
 
-Global Instance decidable_fin (n : nat)
-: Decidable (Fin n).
+Global Instance decidable_fin@{u} (n : nat)
+: Decidable@{u} (Fin n).
 Proof.
   destruct n as [|n]; try exact _.
   exact (inl (inr tt)).
 Defined.
 
-Global Instance decidablepaths_fin@{} (n : nat)
-: DecidablePaths (Fin n).
+Global Instance decidablepaths_fin@{u} (n : nat)
+: DecidablePaths@{u} (Fin n).
 Proof.
   simple_induction n n IHn; simpl; exact _.
 Defined.

diff --git a/theories/Spaces/Int/Core.v b/theories/Spaces/Int/Core.v
@@ -228,7 +228,7 @@ Definition sgn z :=
 
 (* ** Decidable paths and truncation. *)
 
-Global Instance decpaths_int : DecidablePaths Int.
+Global Instance decpaths_int : DecidablePaths@{u} Int.
 Proof.
   intros [n | | n] [m | | m].
   + destruct (dec (n = m)) as [p | q].
@@ -247,4 +247,4 @@ Proof.
 Defined.
 
 (** Since integers have decidable paths they are a hset *)
-Global Instance hset_int : IsHSet Int | 0 := _.
+Global Instance hset_int : IsHSet@{u} Int | 0 := _.
diff --git a/theories/Spaces/Pos/Core.v b/theories/Spaces/Pos/Core.v
@@ -99,7 +99,7 @@ Definition x1_neq_x0 {z w : Pos} : x1 z <> x0 w
 
 (** * Positive binary integers have decidable paths *)
 
-Global Instance decpaths_pos : DecidablePaths Pos.
+Global Instance decpaths_pos : DecidablePaths@{u} Pos.
 Proof.
   intros n; induction n as [|zn|on];
   intros m; induction m as [|zm|om].
@@ -121,7 +121,7 @@ Proof.
 Defined.
 
 (** Decidable paths imply Pos is a hSet *)
-Global Instance ishset_pos : IsHSet Pos := _.
+Global Instance ishset_pos : IsHSet@{u} Pos := _.
 
 (** * Operations over positive numbers *)