1
$\begingroup$

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.

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Mar 23, 2021 at 9:41
  • $\begingroup$ @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. $\endgroup$
    – user61651
    Mar 23, 2021 at 10:04
  • 3
    $\begingroup$ @einzwein There is a type theory Zulip: typ.zulipchat.com $\endgroup$
    – Neel Krishnaswami
    Mar 23, 2021 at 10:41
  • 1
    $\begingroup$ You are not annoying me! I'm just running out of steam. "It's not you, it's me." $\endgroup$
    – Andrej Bauer
    Mar 23, 2021 at 12:48

2 Answers 2

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – user61651
    Mar 30, 2021 at 7:33
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Mar 30, 2021 at 8:03
0
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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$? $\endgroup$
    – user61651
    Mar 23, 2021 at 17:08
  • $\begingroup$ 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ₙ $\endgroup$
    – Stefan
    Mar 23, 2021 at 17:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.