Home

命題

module foundations.proposition where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type

h-proposition、あるいは単に命題(proposition)と呼ばれる型は次のように定義される。

private variable ℓ : Level

isProp : Type ℓ → Type ℓ
isProp A = ∀ (x y : A) → x ＝ y

hProp : (ℓ : Level) → Type (lsuc ℓ)
hProp ℓ = Σ[ A ∈ Type ℓ ] isProp A