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

instance
Lift-instance : ∀ {ℓ ℓ′} {A : Type ℓ} → ⦃ A ⦄ → Lift ℓ′ A
Lift-instance ⦃ x ⦄ = lift x


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

open import Prim.Literals public

auto : ∀ {ℓ} {A : Type ℓ} → ⦃ A ⦄ → A
auto ⦃ a ⦄ = a