module foundations.universe where
まず、Agda.Primitiveモジュールから宇宙レベル関連のものを再エクスポートする。
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Setω to Typeω) public
AgdaはSetという名前で宇宙を提供しているが、HoTT/UF的観点からは集合という言葉は他の用途に使いたいので、Typeという名前にする。
Type : (ℓ : Level) → Set (lsuc ℓ) Type ℓ = Set ℓ