From 3d0916f448ea20dffc64c72c8652e277ce31444d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Fri, 23 Feb 2018 13:20:30 +0100
Subject: [PATCH] Use correct name for hSets

---
 src/Cat/Categories/Sets.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index bc0fd81..035c743 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -19,7 +19,7 @@ module _ (ℓ : Level) where
     open import Cubical.Universe
 
     SetsRaw : RawCategory (lsuc ℓ) ℓ
-    Object SetsRaw = Cubical.Universe.0-Set
+    Object SetsRaw = hSet
     Arrow SetsRaw (T , _) (U , _) = T → U
     𝟙 SetsRaw = Function.id
     _∘_ SetsRaw = Function._∘′_