------------------------------------------------------------------------ -- The Agda standard library -- -- Sizes for Agda's sized types ------------------------------------------------------------------------ module Size where open import Agda.Builtin.Size public renaming ( SizeU to SizeUniv ) -- sort SizeUniv using ( Size -- Size : SizeUniv ; Size<_ -- Size<_ : Size → SizeUniv ; ↑_ -- ↑_ : Size → Size ; ∞ ) -- ∞ : Size