-- A universe is a type whose elements are types.

-- So far, you have seen only one universe: Set

open import Bool
open import Nat

-- The type of an ordinary type is "Set".

some-set : Set
some-set = Bool

-- What is the type of Set?
-- Set : Set₁
-- Set₁ : Set₂
-- Set₂ : Set₃
-- ...

-- Set₁ is a universe whose elements are "proper classes".
-- The "class of all proper classes" is not itself a proper class (because of Russell's paradox).
-- It is a "large class", i.e., a Set₂.

-- Also, Set is just an abbreviation for Set₀


-- To summarize:
-- 
-- true : Bool
-- Bool : Set
-- Set  : Set₁
-- Set₁ : Set₂
-- Set₂ : Set₃

module Short-Logic where

  data True : Set where
    <> : True

  data _×_ (A B : Set) : Set where
    _,_ : A -> B -> A × B

-- ----------------------------------------------------------------------
-- * How do universes come into everyday life?

-- Suppose we want to define function 'Prod', which inputs a list of
-- sets and takes their cartesian product.
--
-- I.e., we want the following:
--
-- Prod (A :: B :: C :: nil) = A × B × C

module Attempt1 where

  data List (A : Set) : Set where
    nil : List A
    _::_ : A -> List A -> List A

  infixr 4 _::_

  {- 
  -- THIS DOES NOT WORK. The error is: Set₁ != Set.
  -- The problem is that A (in the definition of List) cannot be Set,
  -- because we need A : Set, and we don't have Set : Set.
  Prod : List Set -> Set
  Prod = ?
  -}

module Attempt2 where

  open Short-Logic

  data List (A : Set) : Set where
    nil : List A
    _::_ : A -> List A -> List A

  infixr 4 _::_

  data List₁ (A : Set₁) : Set₁ where
    nil : List₁ A
    _::_ : A -> List₁ A -> List₁ A

  -- Prod (A :: B :: C :: nil) = A × (B × (C × True))
  Prod : List₁ Set -> Set
  Prod nil = True
  Prod (A :: As) = A × (Prod As)

  -- This gets awkward. For one, we now have two different list types,
  -- namely List and List₁.
  --
  -- For every function we defined on lists (e.g. reverse, ++, :>, etc.)
  -- we now need to define a "large" version (e.g. reverse₁, ++₁, etc.)

  data List₂ (A : Set₂) : Set₂ where
    nil : List₂ A
    _::_ : A -> List₂ A -> List₂ A

  data True₁ : Set₁ where
    <> : True₁

  data _×₁_ (A B : Set₁) : Set₁ where
    _,_ : A -> B -> A ×₁ B

  Prod₁ : List₂ Set₁ -> Set₁
  Prod₁ nil = True₁
  Prod₁ (A :: As) = A ×₁ (Prod₁ As)

  -- Here is an example of an element of type Set₁ other than Set itself.
  -- very-large-product is an element of type Set₁, and its elements
  -- are pairs (A, B) where A B : Set.
  very-large-product : Set₁
  very-large-product = Set ×₁ Set

  -- Historical fact: when Per Martin-Löf first invented type theory,
  -- he used the typing rule Set : Set.
  -- It took a while, but then Girard proved a contradiction from this.
  -- It's called "Girard's paradox", and is basically a type-theory version
  -- of Russell's paradox.

module Attempt3 where

  -- All of this duplication is awkward. Instead, we use something
  -- called "universe polymorphism".

  open import Agda.Primitive

  -- In the module Agda.Primitive, there is a type "Level".
  --
  -- Set₅ is just an abbreviation for Set ℓ, where ℓ : Level, ℓ = 5.
  --
  -- Note: \ell to type ℓ.

  -- Agda considers Set₁ to be an abbreviation for Set (lsuc lzero)

  data List {ℓ : Level} (A : Set ℓ) : Set ℓ where
    nil : List A
    _::_ : A -> List A -> List A

  data True {ℓ : Level} : Set ℓ where
    <> : True

  -- Type \sqcup for the symbol ⊔, which computes the maximum of two levels.
  data _×_ {ℓ k : Level} (A : Set ℓ) (B : Set k) : Set (ℓ ⊔ k) where
    _,_ : A -> B -> A × B

  -- Compute the (ordinary) product of a list of numbers.
  prod : List ℕ -> ℕ
  prod nil = 1
  prod (x :: xs) = x * (prod xs)

  -- Compute the cartesian product of a list of sets.
  Prod : List Set -> Set
  Prod nil = True
  Prod (A :: As) = A × (Prod As)

  very-large-product : Set₁
  very-large-product = Set × Set

  cannot-do : Set₁
  cannot-do = Set × Bool
  
module Another-Example where

  open import Equality

  -- Rather than defining a monoid by saying what a "monoid structure on a set A is",
  -- we can also define a monoid as an entity in its own right.
  record Monoid : Set₁ where
    field
      A : Set
      plus : A -> A -> A
      unit : A
      associativity-law : ∀ (x y z : A) -> plus (plus x y) z == plus x (plus y z)
      left-unit-law : ∀ (x : A) -> plus unit x == x
      right-unit-law : ∀ (x : A) -> plus x unit == x

  open Monoid

  theorem : ∀ (M : Monoid) -> plus M (unit M) (unit M) == (unit M)
  theorem M = 
      equational plus M (unit M) (unit M)
              by left-unit-law M (unit M)
          equals unit M