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 6 Β¬_

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

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