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 Prim.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.

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π

We re-export the following very important types:

open import Prim.Data.Sigma public
open import Prim.Data.Bool public
open import Prim.Data.Nat hiding (_<_) public


Additionally, we define the empty type:

data β₯ : Type where

absurd : β {β} {A : Type β} β .β₯ β A
absurd ()

Β¬_ : β {β} β Type β β Type β
Β¬ A = A β β₯
infix 3 Β¬_


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


## 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

instance
Lift-instance : β {β β'} {A : Type β} β β¦ A β¦ β Lift β' A
Lift-instance β¦ x β¦ = lift x


## 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
{-# INLINE id #-}

infixr -1 _$_ _$α΅’_ _$β_ _$_ : β {ββ ββ} {A : Type ββ} {B : A β Type ββ} β ((x : A) β B x) β ((x : A) β B x)
f $x = f x {-# INLINE _$_ #-}

_$α΅’_ : β {ββ ββ} {A : Type ββ} {B : .A β Type ββ} β (.(x : A) β B x) β (.(x : A) β B x) f$α΅’ x = f x
{-# INLINE _$α΅’_ #-} _$β_ : β {ββ ββ} {A : Type ββ} {B : A β SSet ββ} β ((x : A) β B x) β ((x : A) β B x)
f $β x = f x {-# INLINE _$β_ #-}

open import Prim.Literals public

auto : β {β} {A : Type β} β β¦ A β¦ β A
auto β¦ a β¦ = a

case_of_ : β {β β'} {A : Type β} {B : Type β'} β A β (A β B) β B
case x of f = f x

case_return_of_ : β {β β'} {A : Type β} (x : A) (B : A β Type β') (f : (x : A) β B x) β B x
case x return P of f = f x

{-# INLINE case_of_        #-}
{-# INLINE case_return_of_ #-}