[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi
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."
http://staff.math.su.se/palmgren/publications.html
http://www2.math.uu.se/~palmgren/universe.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)
mutual
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
mutual
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
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"
Stefan
