From c0cf6789cdfc3585106ffaeb2951e84ffafae309 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 12 Mar 2018 13:56:49 +0100 Subject: [PATCH] Use propositions straight from the horses mouth --- libs/cubical | 2 +- src/Cat/Wishlist.agda | 9 +-------- 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/libs/cubical b/libs/cubical index 3a125a0..5b35333 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit 3a125a0cb010903e6aa80569a0ca5339424eaf86 +Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda index 8a63dc4..67eeccc 100644 --- a/src/Cat/Wishlist.agda +++ b/src/Cat/Wishlist.agda @@ -4,13 +4,6 @@ open import Level open import Cubical.NType open import Data.Nat using (_≤_ ; z≤n ; s≤s) -open import Cubical.NType.Properties public using (propHasLevel) +open import Cubical.NType.Properties postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A - -module _ {ℓ : Level} {A : Set ℓ} where - isSetIsProp : isProp (isSet A) - isSetIsProp = propHasLevel (S (S ⟨-2⟩)) - - propIsProp : isProp (isProp A) - propIsProp = propHasLevel (S ⟨-2⟩)