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