module 1Lab.Type where

UniversesπŸ”—

A universe is a type whose inhabitants are types. In our type theory, the most common universe is Type, the univalent universe of fibrant types.

open import Prim.Type public

Since Type is itself a fibrant type (with composition given by glueing), we might want for it to also live in a universe. However, a universe closed under Ξ£ and W-types, which Type is, can not code for itself: this is Russell’s paradox. Instead, Type is parametrised by a Level, a technical gadget which serves to stratify a hierarchy of universes to prevent any given universe for belonging to itself. In particular, the type Type belongs to a successor universe Type₁, and, in general, the universe lives in the universe.

_ : Type₁
_ = Type

_ : (β„“ : Level) β†’ Type (lsuc β„“)
_ = Ξ» β„“ β†’ Type β„“

Every fibrant type lives in exactly one universe, so we can recover by unification the Level of a given type.

level-of : {β„“ : Level} β†’ Type β„“ β†’ Level
level-of {β„“} _ = β„“

The built-in universes are furthermore all predicative, which in this context means that the domain of a family of types also influences the universe level at which the product of that family lives. To express this, Levels are closed under a binary β€œmax” operator _βŠ”_.

_ : βˆ€ {β„“ β„“'} (A : Type β„“) β†’ (A β†’ Type β„“') β†’ Type (β„“ βŠ” β„“')
_ = Ξ» A B β†’ ((x : A) β†’ B x)

LiftingπŸ”—

We have mentioned that every fibrant type lives in exactly one universe. This is to say that our universes are not cumulative. Instead, we can define (as a record type) a map which Lifts a type to a higher universe. Considered as a function between universes, Lift is an embedding. Moreover, the Lift of a type is definitionally isomorphic to that type.

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

Built-in type formersπŸ”—

The Type universes are closed under Ξ£, and the lowest universe contains both the natural numbers Nat and the booleans Bool.

open import Prim.Data.Sigma public
open import Prim.Data.Bool public
open import Prim.Data.Nat hiding (_<_; _≀_) public

_ = Bool
_ = Nat

_ : βˆ€ {β„“ β„“'} (A : Type β„“) β†’ (A β†’ Type β„“') β†’ Type (β„“ βŠ” β„“')
_ = Ξ£

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

Auxilliary universesπŸ”—

Our type theory has a couple more families of universes that serve to support the formalisation. Above, we wrote down a function type where the universe at which the codomain lives depends on the input value. These β€œlarge” products are classified in TypeΟ‰. These β€œlimit” universes are themselves organised into a hierarchy, but, unlike Type, the indexing of this hierarchy is external: the subscript in Typeω₁ is a literal number, and not shorthand for a value of some type.

_ : Typeω
_ = (β„“ : Level) β†’ Type (lsuc β„“)

_ : Typeω₁
_ = Typeω

The Type universes also code for universes of strict propositions, that is, types which have at most one inhabitant up to definitional equality. We write these universes as SProp. As with Type, these are predicative, in that, while the product of a SProp-valued family will again live in a SProp, the level of the result depends on both the domain and codomain.

_ : βˆ€ {β„“} β†’ Type (lsuc β„“)
_ = SProp _

Some strict propositionsπŸ”—

We populate the smallest SProp universe with analogues of the unit and empty types. These enjoy the property that any of their inhabitants, even hypothetical, are definitionally equal.

record ⊀˒ : SProp where
  instance constructor ttΛ’

data βŠ₯Λ’ : SProp where

The empty Type, βŠ₯, is defined by lifting the empty SProp. Since βŠ₯ is an eta-equality record type, it β€œinherits” definitional irrelevance from βŠ₯Λ’.

record βŠ₯ : Type where
  constructor liftΛ’
  field lowerΛ’ : βŠ₯Λ’

Even defined like this, the empty type has an elimination principle into arbitrary types. We define an eliminator absurd valued in small fibrant types. To demonstrate that the codomain can be arbitrary, we can also define absurdω.

absurd : βˆ€ {β„“} {A : Type β„“} β†’ βŠ₯ β†’ A
absurd ()

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

The negation of a type is, as usual, the type of functions With our setup, the negation of an arbitrary type is definitionally proof-irrelevant.

Β¬_ : βˆ€ {β„“} β†’ Type β„“ β†’ Type β„“
Β¬ A = A β†’ βŠ₯
infix 6 Β¬_

Basic syntactic nicetiesπŸ”—

We close out this module with the definition of a couple helpers which do not depend on anything other than quantification over types. First, we have (dependent) function composition _∘_, and the identity function id.

_∘_
  : βˆ€ {ℓ₁ β„“β‚‚ ℓ₃} {A : Type ℓ₁} {B : A β†’ Type β„“β‚‚} {C : (x : A) β†’ B x β†’ Type ℓ₃}
  β†’ (f : βˆ€ {x} β†’ (y : B x) β†’ C x y) (g : βˆ€ x β†’ B x)
  β†’ βˆ€ x β†’ C x (g x)
(f ∘ g) z = f (g z)

id : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A
id x = x

We also define two helpers for function application. The first, _$_, is familiar from Haskell, and serves simply to adjust precedence: one can write f $ g x instead of f (g x).

infixr -1 _$_

_$_ : βˆ€ {a b} {A : Type a} {B : A β†’ Type b} β†’ ((x : A) β†’ B x) β†’ ((x : A) β†’ B x)
f $ x = f x

The second, case_of_, is a mixfix operator which constraints its function argument to be nondependent, which enables type inference. When given a pattern-matching lambda as its second argument, case_of_ can be used to scrutinise a value in an expression context.

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

_ : Bool β†’ Bool
_ = Ξ» x β†’ case x of Ξ» where
  true  β†’ false
  false β†’ true

Finally, the 1Lab makes extensive use of instance arguments for automation. A convenient entry point to this automation is the auto function, which can be used to call instance search where a visible argument is expected.

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

{-# INLINE id #-}
{-# INLINE _$_ #-}

infixr 40 _∘_
infixr -1 _$β‚›_

_$β‚›_ : βˆ€ {ℓ₁ β„“β‚‚} {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)

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 ⦄)

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