Tip revision: dfb2127
Super.agda
``````
{-# OPTIONS --postfix-projections #-}

{-
Notes on Palmgren's super universe: http://www2.math.uu.se/~palmgren/universe.pdf

We investigate recursive sub-universes and transfinite levels.

Summary of super and Mahlo universes:
(U, El) is *super* if every internal family is contained in an internal sub-universe
(U, El) is *Mahlo* if for every internal (Famᵘ → Famᵘ) operator there is an internal sub-universe closed under it.
-}

module Super where

open import Lib
open import Data.Nat
open import Function

-- simple tree ordinals (Brouwer ordinals) for indexing purposes
data O : Set where
zero : O
suc  : O → O
sup  : (ℕ → O) → O

ℕ→O : ℕ → O
ℕ→O zero    = zero
ℕ→O (suc n) = suc (ℕ→O n)

ω : O
ω = sup ℕ→O

module Cumulative where

-- universe operator
module _ {U : Set}{El : U → Set} where

data UU : Set
EL : UU → Set

data UU where
U'  : UU
El' : U → UU
Π'  : ∀ a → (El a → UU) → UU
ℕ'  : UU

EL U'       = U
EL (El' a)  = El a
EL (Π' a b) = ∀ x → EL (b x)
EL ℕ'       = ℕ

-- super universe
data V : Set
S : V → Set

data V where
UU' : (a : V) → (S a → V) → V
EL' : ∀ {a b} → S (UU' a b) → V
ℕ'  : V
Π'  : (a : V) → (S a → V) → V
Σ'  : (a : V) → (S a → V) → V

S (UU' a b) = UU {S a} {S ∘ b}
S (EL' x)   = EL x
S ℕ'        = ℕ
S (Π' a b)  = ∀ x → S (b x)
S (Σ' a b)  = ∃ (S ∘ b)

VFam : Set
VFam = ∃ λ a → S a → V

û : VFam → VFam
û (a , b) = UU' a b , EL' {a}{b}

û^ : ℕ → VFam
û^ zero    = ℕ' , (λ _ → ℕ')
û^ (suc n) = û (û^ n)

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

Uω' : V
Uω' = UU' ℕ' (₁ ∘ û^)

-- cumulative, non-recursive sub-universes
module NatU where
U : ℕ → Set
El : ∀ {n} → U n → Set
U  zero      = ⊥
U  (suc n)   = UU {U n}{El {n}}
El {suc n} a = EL a

↑ : ∀ {n} → U n → U (suc n)
↑ {suc n} a = El' a

↑El : ∀ {n a} → El (↑ {n} a) ≡ El a  -- not recursive: ↑ ℕ' ≢ ℕ'
↑El {suc n} {a} = refl

-- cumulative, recursive sub-universes (but not transfinite)
module NatU2 where

U : ℕ → Set
El : ∀ {n} → U n → Set
U zero = ⊥
U (suc n) = UU {U n}{El {n}}
El {suc n} U' = U n
El {suc n} (El' a) = El a
El {suc n} (Π' a b) = ∀ x → El (b x)
El {suc n} ℕ' = ℕ

↑ : ∀ {n} → U n → U (suc n)
El≡ : ∀ {n} a → El a ≡ El (↑ {n} a)
↑ {suc n} U'       = El' U'
↑ {suc n} (El' a)  = El' (↑ a)
↑ {suc n} (Π' a b) = Π' (↑ a) λ x → ↑ (b (coe (El≡ a ⁻¹) x))
↑ {suc n} ℕ'       = ℕ'
El≡ {suc n} U' = refl
El≡ {suc n} (El' a) = El≡ a
El≡ {suc n} (Π' a b) rewrite El≡ a =
(λ b → (∀ x → b x)) & (_∋_ ((λ x → El (b x)) ≡ (λ x → El (↑ (b x)))) (ext λ x → El≡ (b x)))
El≡ {suc n} ℕ' = refl

-- transfinite, but non-recursive
module OU where

U : O → Set
El : ∀ {i} → U i → Set
U  zero      = ⊥
U  (suc i)   = UU {U i}{El {i}}
U  (sup f)   = UU {∃ (U ∘ f)}{El ∘ ₂}
El {suc i} a = EL a
El {sup f} a = EL a

foo : U (suc (suc (suc zero)))
foo = Π' U' λ A → Π' (El' A) λ _ → El' (El' A)

ex1 : U ω
ex1 = El' (3 , foo)

ex2 : U ω
ex2 = Π' (3 , foo) λ _ → ℕ'

↑+ : ∀ {i} → U i → U (suc i)
↑+ {i} a = El' a

↑sup : ∀ {f n} → U (f n) → U (sup f)
↑sup {f} {n} a = El' (n , a)

--------------------------------------------------------------------------------
``````