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