module foundations.h-level where
open import foundations.universe open import foundations.natural-number open import foundations.contractible-type open import foundations.proposition open import foundations.identity-type
n-typeの概念を定義するために使う。ただし、n-typeにおけるnは-2から始まるのに対して、h-levelは0から始まる。すなわち、n-typeはn + 2のh-levelを持つことになる。
HLevel : Type lzero HLevel = ℕ
private variable ℓ : Level ofHLevel : HLevel → Type ℓ → Type ℓ ofHLevel zero A = isContr A ofHLevel (suc zero) A = isProp A ofHLevel (suc (suc i)) A = ∀ (x y : A) → ofHLevel (suc i) (x ＝ y)
すなわち、可縮な型はh-levelが0であり、命題はh-levelが1となる。