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 _$_ #-}