module 1Lab.Type where


A universe is a type whose inhabitants are types. In Agda, there is a family of universes, which, by default, is called Set. Rather recently, Agda gained a flag to make Set not act like a keyword, and allow renaming it in an import declaration from the Agda.Primitive module.

open import Agda.Primitive
  renaming (Set to Type ; Setω to Typeω)
  hiding (Prop)

Type is a type itself, so it’s a natural question to ask: does it belong to a universe? The answer is yes. However, Type can not belong to itself, or we could reproduce Russell’s Paradox, as is done in this module.

To prevent this, the universes are parametrised by a Level, where the collection of all β„“-sized types is Type (lsuc β„“):

_ : (β„“ : Level) β†’ Type (lsuc β„“)
_ = Ξ» β„“ β†’ Type β„“

level-of : {β„“ : Level} β†’ Type β„“ β†’ Level
level-of {β„“} _ = β„“

Built-in TypesπŸ”—

Agda comes with built-in definitions for a bunch of types:

open import Agda.Builtin.Sigma hiding (Ξ£) public
open import Agda.Builtin.Unit public
open import Agda.Builtin.Bool public
open import Agda.Builtin.Nat hiding (_<_) public

It does not, however, come with a built-in definition of the empty type:

data βŠ₯ : Type where

absurd : βˆ€ {β„“} {A : Type β„“} β†’ βŠ₯ β†’ A
absurd ()

The dependent sum of a family of types is notated by Ξ£. The domain of the family is left implicit. We use a notation for when it must be made explicit.

Ξ£ : βˆ€ {a b} {A : Type a} (B : A β†’ Type b) β†’ Type _
Ξ£ = Agda.Builtin.Sigma.Ξ£ _

module Ξ£ = Agda.Builtin.Sigma.Ξ£

syntax Ξ£ {A = A} (Ξ» x β†’ B) = Ξ£[ x ∈ A ] B
infix 5 Ξ£

The non-dependent product type _Γ—_ can be defined in terms of the dependent sum type:

_Γ—_ : βˆ€ {a b} β†’ Type a β†’ Type b β†’ Type _
A Γ— B = Ξ£[ _ ∈ A ] B

infixr 4 _Γ—_


There is a function which lifts a type to a higher universe:

record Lift {a} β„“ (A : Type a) : Type (a βŠ” β„“) where
  constructor lift
    lower : A

Function compositionπŸ”—

Since the following definitions are fundamental, they deserve a place in this module:

_∘_ : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃} {A : Type ℓ₁} {B : A β†’ Type β„“β‚‚} {C : (x : A) β†’ B x β†’ Type ℓ₃}
    β†’ (βˆ€ {x} β†’ (y : B x) β†’ C x y)
    β†’ (f : βˆ€ x β†’ B x)
    β†’ βˆ€ x β†’ C x (f x)
f ∘ g = Ξ» z β†’ f (g z)

infixr 40 _∘_

id : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A
id x = x

infixr -1 _$_

_$_ : βˆ€ {ℓ₁ β„“β‚‚} {A : Type ℓ₁} {B : A β†’ Type β„“β‚‚} β†’ ((x : A) β†’ B x) β†’ ((x : A) β†’ B x)
f $ x = f x
{-# INLINE _$_ #-}