[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


In my PhD thesis (Uppsala University 1991) I consider transfinite hierarchies of type universes in Martin-Löf type theory. Some of this was published in a 1998 proceedings:

"On universes in type theory, in: G. Sambin and J. Smith (eds.) Twenty Five Years of Constructive Type Theory. Oxford Logic Guides, Oxford University Press 1998, 191-204 (refereed collection of papers). Near final version in PDF."



The so-called superuniverses (V,S) (which admits transfinite iterations of universes) have been formalized in Agda. Here is an example of such a formalization:


-- building a universe above a family (A,B)

  data U (A : Set) (B : A -> Set) : Set where
     n₀ : U A B
     n₁ : U A B
     ix : U A B
     lf : A -> U A B
     _⊕_ : U A B -> U A B -> U A B
     σ : (a : U A B) -> (T a -> U A B) -> U A B
     π : (a : U A B) -> (T a -> U A B) -> U A B
     n : U A B
     w : (a : U A B) -> (T a -> U A B) -> U A B
     i : (a : U A B) -> T a -> T a -> U A B

  T : {A : Set} {B : A -> Set} ->  U A B -> Set
  T n₀              = N₀
  T n₁              = N₁
  T {A} {B} ix      = A
  T {A} {B} (lf a)  = B a
  T (a ⊕ b)         = T a + T b
  T (σ a b)         = Σ (T a) (\x -> T (b x))
  T (π a b)         = Π (T a) (\x -> T (b x))
  T n               = N
  T (w a b)         = W (T a) (\x -> T (b x))
  T (i a b c)       = I (T a) b c

-- the super universe (V, S): a universe which is closed also
-- under the above universe building operation

  data V : Set where
     n₀ : V
     n₁ : V
     _⊕_ : V -> V -> V
     σ : (a : V) -> (S a -> V) -> V
     π : (a : V) -> (S a -> V) -> V
     n : V
     w : (a : V) -> (S a -> V) -> V
     i : (a : V) -> S a -> S a -> V
     u : (a : V) -> (S a -> V) -> V
     t : (a : V) -> (b : S a -> V) -> U (S a) (\x -> S (b x))  -> V

  S : V -> Set
  S n₀        = N₀
  S n₁        = N₁
  S (a ⊕ b)   = S a + S b
  S (σ a b)   = Σ (S a) (\x -> S (b x))
  S (π a b)   = Π (S a) (\x -> S (b x))
  S n         = N
  S (w a b)   = W (S a) (\x -> S (b x))
  S (i a b c) = I (S a) b c
  S (u a b)   = U (S a) (\x -> S (b x))
  S (t a b c) = T {S a} {\x -> S (b x)} c

There is also work by Anton Setzer (Swansea U) of type universes that go far beyond this, Mahlo universes - a kind of ultimate universe polymorphism. These are significant constructions in proof theory.

Best Regards


Erik Palmgren
Prof Mathematical Logic
Department of Mathematics
Stockholm University

Den 2018-07-10 kl. 23:50, skrev Stefan Monnier:
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Most type theory-based tools nowadays are based on a calculus with an
infinite hierarchy of predicative universes.  Some of them, such as
Agda, also allow abstraction over those levels, so we end up with a PTS
along the lines of:

     ℓ ::= z | s ℓ | ℓ₁ ∪ ℓ₂ | l      (where `l` is a level variable)

     S = { Type ℓ, Type ω, SortLevel }
     A = { Type ℓ : Type (ℓ + 1), TypeLevel : SortLevel }
     R = { (Type ℓ₁, Type ℓ₂, Type (ℓ₁ ∪ ℓ₂)),
           (SortLevel, Type ℓ, Type ω),
           (SortLevel, Type ω, Type ω) }

I was wondering if there's been work to push this to larger ordinals, to
allow maybe rules like

           (Type ω, Type ω, Type (ω·ω))

I.e. "deep universe polymorphism"


Reply via email to