# Explicit type system with infinite non-cumulative universe hierarchy

Is there an open-source proof assistant or at least an explicit set of rules written down somewhere for a type system with an infinite non-cumulative universe hierarchy and unique typing?

I want to see the rules for the universe lifting function spelled out.

• Agda. But I am going to say this again: you are asking many "small" questions, some of which are border-line research level. I do not know what the official policy is regarding chainining question on a narrow topic, but you have pretty much exhausted my energy to keep answering them. I do not mean to ignore you, but I do recommend that for such easy questions you visit one of the more interactive forums, such as Agda Zulip or HoTT Zulip. Mar 23 at 9:41
• @AndrejBauer Sorry for annoying you but I just wasn't sure if I could ask non-homotopy specific questions in the HoTT Zulip. If there was a general type theory Zulip I would probably ask there.
– user61651
Mar 23 at 10:04
• @einzwein There is a type theory Zulip: typ.zulipchat.com Mar 23 at 10:41
• You are not annoying me! I'm just running out of steam. "It's not you, it's me." Mar 23 at 12:48

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.

• In this paper types are not terms of universes but a separate notion. I would prefer a type system where that's not the case.
– user61651
Mar 30 at 7:33
• I think you're a bit too dismissive about the paper. You "wanted" to see the rules for the universe lifting function spelled out, and that's precisely what the paper does (Definition 3.2 spells out the lifting operations and their equations, Theorem 3.4 shows uniqueness of typing). And you are wrong about saying that types are not terms of a universe. Mar 30 at 8:03

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 function". If you want to lift a type from one universe to another you can wrap it in an inductive type which contains a large enough dummy side-info to "push" the result up to the level you want, so the "lift" can be encoded without having to add it explicitly to the system.

• I don't get the second paragraph. So I have the empty type and the unit type in $U_0$. How do I lift them to $U_1$?
– user61651
Mar 23 at 17:08
• Say you have a $V : T : U_0$, you can turn that into $lift~V : Lift~T : U_{n+2}$ by defining something like type Lift (t : U₀) = lift' (dummy : Uₙ₊₁) t and lift = lift' Uₙ Mar 23 at 17:22