module 1Lab.Type where


# Universesπ

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)
public


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 _Γ_


## Liftingπ

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

record Lift {a} β (A : Type a) : Type (a β β) where
constructor lift
field
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 _$_ #-}