From a53efef370bcd166562e1cbf4a2974dc6c154e5e Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 10 Jan 2024 09:00:16 -0500
Subject: [PATCH] Free up universe in proofs of IsHSet, Decidable and
 DecidablePaths

---
 theories/Spaces/Finite/Fin.v | 8 ++++----
 theories/Spaces/Int/Core.v   | 4 ++--
 theories/Spaces/Pos/Core.v   | 4 ++--
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index b81e7e0236a..9d3d5b537b2 100644
--- 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
index 4b90aba6d6a..6c65173b406 100644
--- 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
index a76ffe22853..9cffead5505 100644
--- 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 *)