module Prim.Type where

Primitives: Sorts🔗

This module defines bindings for the primitive sorts. These are very magic symbols since they bootstrap everything about the type system. For more details about the use of universes, see 1Lab.Type.

{-# BUILTIN TYPE      Type  #-}
{-# BUILTIN TYPEOMEGA Typeω #-}

{-# BUILTIN PROP      SProp  #-}
{-# BUILTIN PROPOMEGA SPropω #-}

{-# BUILTIN STRICTSET      SSet  #-}
{-# BUILTIN STRICTSETOMEGA SSetω #-}

Additionally, we have the Level type, of universe levels. The universe levels are an algebra containing 0, closed under successor and maximum. The difference between this and e.g. the natural numbers is that Level isn’t initial, i.e. you can’t pattern-match on it.

postulate
  Level : Type
  lzero : Level
  lsuc  : Level → Level
  _⊔_   : Level → Level → Level
infixl 6 _⊔_

{-# BUILTIN LEVELUNIV LevelUniv #-}
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}