From 8f67ff9f363779fef4a41969b45364682ede4dde Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 21 Mar 2018 15:01:31 +0100
Subject: [PATCH] Use explicit parameter for hSet

---
 src/Cat/Categories/Sets.agda |  8 +++-----
 src/Cat/Prelude.agda         | 15 +++++++++++++--
 2 files changed, 16 insertions(+), 7 deletions(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index a54cba1..75ff8b0 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -59,10 +59,8 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
 
 module _ (ℓ : Level) where
   private
-    open import Cubical.Universe using (hSet) public
-
     SetsRaw : RawCategory (lsuc ℓ) ℓ
-    RawCategory.Object SetsRaw = hSet {ℓ}
+    RawCategory.Object SetsRaw = hSet ℓ
     RawCategory.Arrow  SetsRaw (T , _) (U , _) = T → U
     RawCategory.𝟙      SetsRaw = Function.id
     RawCategory._∘_    SetsRaw = Function._∘′_
@@ -79,7 +77,7 @@ module _ (ℓ : Level) where
     arrowsAreSets {B = (_ , s)} = setPi λ _ → s
 
     isIso = Eqv.Isomorphism
-    module _ {hA hB : hSet {ℓ}} where
+    module _ {hA hB : hSet ℓ} where
       open Σ hA renaming (proj₁ to A ; proj₂ to sA)
       open Σ hB renaming (proj₁ to B ; proj₂ to sB)
       lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f)
@@ -284,7 +282,7 @@ module _ (ℓ : Level) where
     univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB)
     univalent' hA = {!!} , {!!}
 
-    module _ {hA hB : hSet {ℓ}} where
+    module _ {hA hB : hSet ℓ} where
 
       -- Thierry: `thr0` implies univalence.
       univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index d936e60..c17fda0 100644
--- a/src/Cat/Prelude.agda
+++ b/src/Cat/Prelude.agda
@@ -17,7 +17,7 @@ open import Cubical.GradLemma
   using (gradLemma)
   public
 open import Cubical.NType
-  using (⟨-2⟩)
+  using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel)
   public
 open import Cubical.NType.Properties
   using
@@ -25,7 +25,18 @@ open import Cubical.NType.Properties
     ; propPi ; propHasLevel ; setPi ; propSet)
   public
 open import Cubical.Sigma using (setSig ; sigPresSet) public
-open import Cubical.Universe using (hSet) public
+
+module _ (ℓ : Level) where
+  -- FIXME Ask if we can push upstream.
+  -- A redefinition of `Cubical.Universe` with an explicit parameter
+  _-type : TLevel → Set (lsuc ℓ)
+  n -type = Σ (Set ℓ) (HasLevel n)
+
+  hSet : Set (lsuc ℓ)
+  hSet = ⟨0⟩ -type
+
+  Prop : Set (lsuc ℓ)
+  Prop = ⟨-1⟩ -type
 
 -----------------
 -- * Utilities --