module 1Lab.Prim.Type where

Primitives: Sorts🔗

This module defines bindings for the primitive sorts in Agda. 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 PROP Prop #-}
{-# BUILTIN SETOMEGA Typeω #-}
{-# 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 LEVEL Level #-}
{-# BUILTIN LEVELZERO lzero #-}
{-# BUILTIN LEVELSUC lsuc #-}
{-# BUILTIN LEVELMAX _⊔_ #-}