fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Use propositions straight from the horses mouth

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-12 13:56:49 +01:00
parent a7214fcc66
commit c0cf6789cd
2 changed files with 2 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
libs/cubical

@ -1 +1 @@
Subproject commit 3a125a0cb010903e6aa80569a0ca5339424eaf86 Subproject commit 5b35333dbbd8fa523e478c1cfe60657321ca38fe

9
src/Cat/Wishlist.agda
View file

@ -4,13 +4,6 @@ open import Level
open import Cubical.NType open import Cubical.NType
open import Data.Nat using (_≤_ ; z≤n ; s≤s) 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 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⟩)