------------------------------------------------------------------------
-- Support for sized types
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --sized-types #-}

module Prelude.Size where

open import Prelude

-- Size primitives.

open import Agda.Builtin.Size public
  using (Size; ∞)
  renaming (Size<_ to Size<; SizeUniv to Size-universe; ↑_ to ssuc)

-- If S is a type in the size universe, then S in-type is a type in
-- Type.

record _in-type (S : Size-universe) : Type where
  field
    size : S

open _in-type public