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