Universes.agda

{-# OPTIONS --postfix-projections --without-K #-}

-- Notes for https://www.youtube.com/watch?v=RXKRepPm0ps

-- checked with Agda 2.6.1 + stdlib 1.5

open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)
open import Relation.Binary.PropositionalEquality
  renaming (subst to tr; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; cong to ap)
open import Data.Nat
open import Function
open import Induction.WellFounded public

--------------------------------------------------------------------------------

-- link to paper: https://arxiv.org/abs/2103.00223

-- FSCD submission: model lots of universe features: ordinal-bounded hierarchy,
--   cumulativity, internal type for levels with elimination principle
--                 Agda: Level : Set₀
--   universe-polymorphism: (quantify over levels and level bounds using Π types)
--   Coq-style cumulativity (by coercive cumulative subtyping)
--       A        : Set₀
--       A        : Set₁
--       coercive : lift A : Set₁
--   (All of this can be modeled with U+IR)

-- Stronger universes in MLTT
--   ω*ω, etc.
-- Idea: try to model some large cardinal axioms using type theoretic rules
-- Predicative & constructive versions of large cardinal axioms
--   predicative vs. impredicative: former can be analyzed in a useful way
--                                  latter is completely hopeless


-- Grothendieck, Super, Mahlo, IR, ordinal-indexed universe
-- model of TT with internal type of levels

--------------------------------------------------------------------------------

coe : ∀ {α}{A B : Set α} → A ≡ B → A → B
coe refl x = x

coe∘ : ∀ {i}{A B C : Set i}(p : B ≡ C)(q : A ≡ B)(a : A)
       → coe p (coe q a) ≡ coe (q ◾ p) a
coe∘ refl refl _ = refl

◾-inv : ∀ {i}{A : Set i}{a b : A}(p : a ≡ b) → p ◾ p ⁻¹ ≡ refl
◾-inv refl = refl

postulate
  ext : ∀{i j}{A : Set i}{B : A → Set j}{f g : (x : A) → B x}
        → ((x : A) → f x  ≡ g x) → f ≡ g

  exti : ∀{i j}{A : Set i}{B : A → Set j}{f g : ∀ {x} → B x}
          → ((x : A) → f {x} ≡ g {x}) → (λ {x} → f {x}) ≡ g

Π≡ : ∀ {i j}
       {A₀ A₁ : Set i}                      (A₀₁ : A₀ ≡ A₁)
       {B₀ : A₀ → Set j}{B₁ : A₁ → Set j}   (B₀₁ : ∀ a₀ → B₀ a₀ ≡ B₁ (coe A₀₁ a₀))
     → ((x : A₀) → B₀ x) ≡ ((x : A₁) → B₁ x)
Π≡ refl B₀₁ rewrite ext B₀₁ = refl

unAcc : ∀ {α β A R i} → Acc {α}{β}{A} R i → ∀ j → R j i → Acc R j
unAcc (acc f) = f

Acc-prop : ∀ {α β A R i}(p q : Acc {α}{β}{A} R i) → p ≡ q
Acc-prop (acc f) (acc g) = ap acc (ext λ j → ext λ p → Acc-prop (f j p) (g j p))

--------------------------------------------------------------------------------

-- Idea: weaker universes --> stronger universe --> IR (strongest)
--   Assumption: Agda Set₀ (view Set₀ as Type, El in some ambient theory)
--   We just use IR to model the different univs

Fam : Set₁
Fam = Σ Set λ A → A → Set

FamMorph : Fam → Fam → Set₁
FamMorph (U , El) (U' , El') = ∃ λ (f : U → U') → ((a : U) → El a ≡ El' (f a))

-- internal family
Famⁱ : Fam → Set
Famⁱ (U , El) = Σ U λ A → (El A → U)

-- a set is contained in a family:
Elemˢᶠ : Set → Fam → Set₁
Elemˢᶠ A (U , El) = ∃ λ A' → El A' ≡ A    -- (we could also have iso)

-- family contained in a family
Elemᶠᶠ : Fam → Fam → Set₁
Elemᶠᶠ (A , B) U = Elemˢᶠ A U × (∀ a → Elemˢᶠ (B a) U)

-- universe          : Fam closed under basic type formers (ℕ, Π, etc...)
-- subuniv           : FamMorph U U'

-- recursive subuniv : FamMorph where (f : U → U') preserves type formers
--                        f (Π' A B) ≡ Π' (f A) (f B)

-- internal subuniv  : internal family in U which is a sub-univ of U
--          (U, El) : Fam
--          (u, el) : Famⁱ (U, El)


module SimpleUniv where

  -- Closed under type formers.
  -- α is 0-inaccessible if ∀ β < α, 2^β < α    (closed under powersets)
  --     set theory: 2^β ~ Pow(β)
  --       LEM + powersets --> impredicative

  data u : Set
  el : u → Set

  data u where
    ℕ' : u
    Π' : (A : u) → (el A → u) → u

  el ℕ'       = ℕ
  el (Π' A B) = ∀ a → el (B a)

  -- large elimination, polymorphic function over u
  --   (u : Ty Γ) El
  --   (A : u) → ...


module Grothendieck where
  -- (U, El) Grothendieck

  -- Every (A : U) is in an internal sub-universe of U
  -- (U, El) is *not* an internal sub-universe of (U, El)     ≤ (external sense)

  -- α is 1-inaccessible if
  --     - α is 0-inaccessible
  --     - for every β < α, there is 0-inaccessible γ, s.t. β < γ < α

  -- "universe operator"
  module _ (U : Set) where
    data u : Set
    el : u → Set

    data u where
      ℕ' : u
      Π' : (A : u) → (el A → u) → u
      U' : u

    el ℕ'       = ℕ
    el (Π' A B) = ∀ a → el (B a)
    el U'       = U

  -- Grothendieck U
  data U : Set
  El : U → Set

  data U where
    ℕ' : U
    Π' : (A : U) → (El A → U) → U
    u' : U → U                      -- u' A yields an internal sub-universe of U

  El ℕ'       = ℕ
  El (Π' A B) = ∀ a → El (B a)
  El (u' A)   = u (El A)

  -- yields (recursive) internal sub-universe
  --    (in model of TT: recursive sub-U corresponds to Lift which preserves type formers)
  -- alternative: el' : (A : U) → El (u' A) → U as constructor (easier as well)

  el'  : ∀ {A : U} → El (u' A) → U
  el'≡ : ∀ {A}(a : El (u' A)) → el _ a ≡ El (el' a)
  el' ℕ'        = ℕ'
  el' (Π' a b)  = Π' (el' a) λ α → el' (b (coe (el'≡ a ⁻¹) α))
  el' {A} U'    = A
  el'≡ ℕ'       = refl
  el'≡ (Π' a b) = Π≡ (el'≡ a) λ α → el'≡ (b α)
                   ◾ ap (El ∘ el' ∘ b) (ap (λ p → coe p α) (◾-inv (el'≡ a)) ⁻¹)
                   ◾ ap (El ∘ el' ∘ b) (coe∘ (el'≡ a ⁻¹)(el'≡ a) α ⁻¹)
  el'≡ U'       = refl


  -- u' ℕ'           < U
  -- u' (u' ℕ')      < U
  -- u' (u' (u' ℕ')) < U
  -- not cumulative! (not sub-universes of each other)

   -- flattened hierarchy

   --          U
   -- u'₀, u'₁, u'₂, u', u'

  u0 = u' ℕ'
  u1 = u' u0 --- U' symbol for u0
  u2 = u' u1

  fun : El u1
  fun = Π' U' λ A → {!!}

  el01 : El u0 → El u1   -- embedding from u0 to u1
  el01≡ : ∀ (A : El u0) → el _ A ≡ el _ (el01 A)
  el01 ℕ'       = ℕ'
  el01 (Π' A B) = Π' (el01 A) λ a → el01 (B (coe (el01≡ A ⁻¹) a))
  el01 U'       = U'
  el01≡ ℕ'       = refl
  el01≡ (Π' A B) = trivial where postulate trivial : _
  el01≡ U'       = {!!} -- ℕ ≢ u ℕ !!

  uₙ : ℕ → U
  uₙ n = u' (case n of λ {0 → ℕ'; (suc n) → uₙ n})

  -- we can quantify over uₙ types in large U
  f : U
  f = Π' ℕ' λ n → Π' (uₙ n) λ A → Π' (el' A) λ _ → el' A

  -- we can manipulate (u n) in u (suc n), but can't decode
  A : El u1
  A = Π' U' λ _ → U'   -- function type u0 → u0


module Super where
  -- Palmgren (Rathjen about ordinal analysis of super univ)

  -- Every (F : Famⁱ U) is in an internal sub-universe of U

  -- We can send (F : Famⁱ U) to (reflect F : Famⁱ U), s.t. F' is a universe
  -- reflect (reflect (reflect F))
  -- we can iterate this: reflect^α F is a cumulative hierarchy.
  -- if we have infinitary types in U: transfinite cumulative hierarchy

  -- universe operator
  module _ (U : Set)(El : U → Set) where

    data u : Set
    el : u → Set

    data u where
      ℕ'  : u
      Π'  : (A : u) → (el A → u) → u
      u'  : u
      el' : U → u

    el ℕ'       = ℕ
    el (Π' A B) = ∀ x → el (B x)
    el u'       = U
    el (el' A)  = El A

  data U : Set
  El : U → Set

  -- reflect : Famᴵ U → Famᴵ U

  data U where
    ℕ'  : U
    Π'  : (A : U) → (El A → U) → U
    u'  : (A : U) → (El A → U) → U
    el' : ∀ {A : U}{B : El A → U} → El (u' A B) → U  -- not ind-ind!

  El ℕ'             = ℕ
  El (Π' A B)       = ∀ x → El (B x)
  El (u' A B)       = u (El A) (El ∘ B)
  El (el' {A}{B} a) = el _ _ a

  -- cumulative countable universes:
  û : Famⁱ (U , El) → Famⁱ (U , El)
  û (A , B) = (u' A B) , el' {A}{B}

  uₙ : ℕ → Famⁱ (U , El)
  uₙ zero    = ℕ' , (λ _ → ℕ')
  uₙ (suc n) = û (uₙ n)

  uω : U
  uω = u' {!!} {!!}

  -- -- -- codes for some transfinite universes
  -- -- Uω : V
  -- -- Uω = UU' (Σ' ℕ' λ n → û^ n .₁) (λ {(n , a) → û^ n .₂ a})

  -- -- Uω' : V
  -- -- Uω' = UU' ℕ' (₁ ∘ û^)

  -- data O : Set where
  --   zero : O
  --   suc : O → O
  --   lim : (ℕ → O) → O


module Mahlo where
  -- (U, El) is Mahlo if
  -- For every (F : Famⁱ U → Famⁱ U) there is an internal sub-universe of U closed under F
  --    reflect : (Famⁱ U → Famⁱ U) → Famⁱ U
  --     s.t  (G : Famⁱ U)    G is contained in reflect F    then    F G is contained in (reflect F)

  -- κ is α-inaccessible: for all β < α, β-inacessibles are unbounded below κ
  -- κ is hyper-0-inaccessible: κ is κ-inaccessible
  -- κ is hyper-1-inaccessible ...
  -- κ is hyper-hyper-0-inaccessible ...
  -- κ is hyper^α-inaccessible ...
  -- κ is Mahlo : κ is hyper^κ-inaccessible

  -- There is no internal inductive U in Agda, s.t. U is Mahlo (not strictly positive definition!)
  -- but Set itself is Mahlo.

  -- reflect : (Famⁱ U → Famⁱ U) → Famⁱ U   is not strictly positive!
  --  a Mahlo universe is not inductive (does not support induction on type codes)
  -- Agda: Setᵢ supports IR, therefore Setᵢ is Mahlo

  -- (Set) is Mahlo

-- Idris2 bug:

{-
data Fun (F : Type → Type) : Type where

app : Type → Type → Type
app (Fun F) = F
app _       = id

omega : Type
omega = ...
-}

-- IR
--------------------------------------------------------------------------------

-- IR is at least as strong as Mahlo, but upper bound is not known precisely
-- "autonomous Mahlo" is also IR-definable, but stronger than Mahlo
--
--
-- autonomous Mahlo         (Setzer)
-- large IR
-- Π₃-reflecting universe   (Setzer)
-- ? ? ?

-- other stuff:   model transfinite / level polymorphic / internal levels in TT

-- why have fancy universe features, if we can just add IR?
--   "native" features: level inference, implicit coercion (subtyping), convenient

-- Inductive families vs. W-types and Id types

-- Issue: we pick any ordinal α, we want cumulative hierarchy indexed by β < α,
--  i < j,  U i should be recursive sub-universe of U j
--  Lift, Lift should preserve type formers (+ term formers)

-- Problem: Super, Mahlo, it's not known how to combine transfinite + recursive sub-univ
--    recursive embedding: u i,  u j   (internally to a Super universe)
--       (OK if i and j are finite)
--       (Doesn't work if    u i < u ω )

-- Solution: