[Agda] Formalization of Agda's universe polymorphism

[Stefan Monnier]

Could someone point me to some formal presentation of Agda's universe
polymorphism, ideally an article somewhere with soundness proof or
something like that.


Stefan

[Jesper Cockx]

Hi Stefan,

As far as I know there is no such thing, unfortunately. The closest thing
is the work by Matthieu Sozeau on universe polymorphism in Coq (see
https://www.irif.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf).
However, Agda's universe polymorphism allows some more things than Coq,
such as computing universe levels from a term and having
universe-polymorphic module parameters, which do not have a solid
theoretical justification that I know of.

-- Jesper

Post by Stefan Monnier
Could someone point me to some formal presentation of Agda's universe
polymorphism, ideally an article somewhere with soundness proof or
something like that.
Stefan
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Roman]

"On Universes in Type Theory", Erik Palmgren [1] -- is one related
paper. It describes a Tarski-style tower of universes and then adds a
super universe to this tower.

Agda has a Russell-style tower of noncumulative universes. As the paper states:

The Russell formulation should be regarded as an informal version
of the Tarski formulation

Agda also has a super universe, because `∀ α -> Set α` is a legal type
in Agda (but not a legal term), but that super universe is only closed
over `∀` since `∃ λ α -> Set α` is rejected.

I translated a part of the paper to Agda: [2] (universes are
cumulative). This should be easier to read, but take it with a grain
of salt.

[1] http://www2.math.uu.se/~palmgren/universe.pdf
[2] https://github.com/effectfully/random-stuff/blob/master/Omega.agda