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, 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πŸ”—

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

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
{-# 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 β†’ SSet β„“β‚‚} β†’ ((x : A) β†’ B x) β†’ ((x : A) β†’ B x)
f $β‚› x = f x
{-# INLINE _$β‚›_ #-}