Home

h-levelを持つということは命題である

module foundations.proposition-h-level where
Imports 
open import foundations.universe
open import foundations.contractible-type
open import foundations.proposition
open import foundations.h-level
open import foundations.natural-number
open import foundations.identity-type
open import foundations.h-level-pi
open import foundations.greater-h-levels
open import foundations.function-extensionality
open import foundations.sigma-type
open import foundations.sigma-type-identity
open import foundations.transport
open import foundations.set

private variable
  ℓ : Level

module _ (e : FunExtLevel ℓ ℓ) where
  isPropIsContr : ∀ {A : Type ℓ} → isProp (isContr A)
  isPropIsContr {A = A} (c , f) (d , g) =
    toΣId (f d , byFunExtType e _ g λ x → s d x _ (g x))
    where
      s : isSet A
      s = isProp⇒isSet (isContr⇒isProp (c , f))

  isPropIsProp : ∀ {A : Type ℓ} → isProp (isProp A)
  isPropIsProp f = isPropΠ2 e (λ a b → isProp⇒isSet f a b) f

  isPropOfHLevel : ∀ {A : Type ℓ} n → isProp (ofHLevel n A)
  isPropOfHLevel zero = isPropIsContr
  isPropOfHLevel (suc zero) = isPropIsProp
  isPropOfHLevel (suc (suc n)) = isPropΠ2 e λ a b → isPropOfHLevel (suc n)

  isPropIsSet : ∀ {A : Type ℓ} → isProp (isSet A)
  isPropIsSet = isPropOfHLevel 2