New answers tagged proof-assistants
0
Ali Asaf worked out a hierachy of universes with explicit coercions (lifting) in A calculus of constructions with explicit subtyping and established a relationship with cummulative universes.
0
I haven't found a clear set of rules for such a system (including for Agda, tho the source code admittedly should count), so in my paper Is Impredicativity Implicitly Implicit?. I wrote what I understand of Agda's rules (and according to one of the reviewers it's about right).
But I don't know what you mean by "the rules for the universe lifting ...
Top 50 recent answers are included
