Home

集合

module foundations.set where
Imports 
open import foundations.universe
open import foundations.h-level
open import foundations.sigma-type

h-set、あるいは単に集合(set)とは、任意の二点間の同一視型が命題であるような型のことである。

private variable ℓ : Level

isSet : Type ℓ → Type ℓ
isSet = ofHLevel 2

hSet : (ℓ : Level) → Type (lsuc ℓ)
hSet ℓ = Σ[ A ∈ Type ℓ ] isSet A