From bec5acdc59ca50377252399fdaa06bfaf9c287c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 19 Feb 2018 11:25:16 +0100
Subject: [PATCH] Move proposition to wishlist

---
 src/Cat/Category.agda | 6 ++----
 src/Cat/Wishlist.agda | 5 +++++
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index cee681f..1b542be 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -14,6 +14,8 @@ import Function
 open import Cubical
 open import Cubical.NType.Properties using ( propIsEquiv )
 
+open import Cat.Wishlist
+
 ∃! : ∀ {a b} {A : Set a}
   → (A → Set b) → Set (a ⊔ b)
 ∃! = ∃!≈ _≡_
@@ -23,10 +25,6 @@ open import Cubical.NType.Properties using ( propIsEquiv )
 
 syntax ∃!-syntax (λ x → B) = ∃![ x ] B
 
--- This follows from [HoTT-book: §7.1.10]
--- Andrea says the proof is in `cubical` but I can't find it.
-postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)
-
 record RawCategory (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
   -- adding no-eta-equality can speed up type-checking.
   -- ONLY IF you define your categories with copatterns though.
diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda
index 2e56a27..7103b9d 100644
--- a/src/Cat/Wishlist.agda
+++ b/src/Cat/Wishlist.agda
@@ -1,6 +1,11 @@
 module Cat.Wishlist where
 
+open import Level
 open import Cubical.NType
 open import Data.Nat using (_≤_ ; z≤n ; s≤s)
 
 postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A
+
+-- This follows from [HoTT-book: §7.1.10]
+-- Andrea says the proof is in `cubical` but I can't find it.
+postulate isSetIsProp : {ℓ : Level} → {A : Set ℓ} → isProp (isSet A)