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 6 Β¬_

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 5 _Γ—_

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
open Lift public

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 β†’ 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

∘-closed
  : (βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ (A β†’ B) β†’ Type (β„“ βŠ” β„“')) β†’ TypeΟ‰
∘-closed P =
  βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“'} {C : Type β„“''}
    {f : B β†’ C} {g : A β†’ B}
  β†’ P f β†’ P g β†’ P (f ∘ g)

auto : βˆ€ {β„“} {A : Type β„“} β†’ ⦃ A ⦄ β†’ A
auto ⦃ a ⦄ = a

case_of_ : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ A β†’ (A β†’ B) β†’ B
case x of f = f x

case_return_of_ : βˆ€ {β„“ β„“'} {A : Type β„“} (x : A) (B : A β†’ Type β„“') (f : (x : A) β†’ B x) β†’ B x
case x return P of f = f x

{-# INLINE case_of_        #-}
{-# INLINE case_return_of_ #-}

instance
  Number-Lift : βˆ€ {β„“ β„“'} {A : Type β„“} β†’ ⦃ Number A ⦄ β†’ Number (Lift β„“' A)
  Number-Lift {β„“' = β„“'} ⦃ a ⦄ .Number.Constraint n = Lift β„“' (a .Number.Constraint n)
  Number-Lift ⦃ a ⦄ .Number.fromNat n ⦃ lift c ⦄ = lift (a .Number.fromNat n ⦃ c ⦄)

absurdΟ‰ : {A : TypeΟ‰} β†’ .βŠ₯ β†’ A
absurdω ()

infixr -1 primForce
primitive
  primForce : βˆ€ {a b} {A : Type a} {B : A β†’ Type b} (x : A) (f : βˆ€ x β†’ B x) β†’ B x

syntax primForce x f = f $! x