open import Paths
def isProp (A : Type) ⇒ ∀ (a b : A) → a = b
def isSet (A : Type) : Type ⇒ ∀ (a b : A) → isProp (a = b)

def HProp ⇒ Σ (A : Type) ** isProp A
def HSet ⇒ Σ (A : Type) ** isSet A

open import Arith::Nat::Core
def isHLvl Nat Type : Type
| 0, A ⇒ isContr A
| 1, A ⇒ isProp A
| suc n, A ⇒ ∀ (a b : A) → isHLvl n (a = b)