Will the possibility of adding sorts be part of Rocq 1 which , from what I understood should arrive around new years / mars ?

Will it be possible to add subtyping, like I add U + univalence and I declare Type_i <= U_i ?

*Rocq 9, not Rocq 1

There is no subsorting relation right now. Not sure if this is a good idea :)

I don't see the advantage of having two different axes for a universe level. Why not have a variable which represents the pair? In fact, isn't that exactly what Coq used to do?

certainly that would be a lot less notationally cumbersome

At least in the typing rules it makes a lot of sense to separate the two.

Say you have a predicative `Prop`

then I guess `Prop i`

lives in `Type (i + 1)`

so the separation is useful. Also the level of a dependent product depends only on the levels, but not the kinds of universes (or qualities, or sorts).

From a notational perspective, I see your point that it's quite verbose.

I mean, you can have a level that means `Prop i`

and a level that means `Type (i+1)`

and the first one is `<`

the second one; this doesn't stop you from having two universe hierarchies if you want

i.e. universes form a partial order and level variables quantify over the elements of this partial order

Sure. But I mean, there is a practicality in dissociating the two I think?

The only thing is that you may want to have restrictions that a sort is only of the form `Type i`

and not `Prop`

or vice versa, which is what is done in the current system by specifying the sort variable but not the level variable

You could also want to be polymorphic in the sort but not the level? Maybe. :sweat_smile:

you might want to have an arbitrary universe which is contained in a specified one, but that's basically already covered by level inequality constraints

to me it looks like coq belatedly getting something equivalent to lean's universe polymorphism, only worse because of path-dependent reasons

I will grant that having level 0 be special magic, and using the `imax u v = if v = 0 then 0 else max u v`

function to define pi types, is a bit weird, but doubling the number of universe variables in the average piece of code (which cares about none of them) seems worse

especially since coq is known for having issues keeping universe inference under control

Yeah, I agree that having `Prop i = Prop j`

is ok on the meta-theory maybe (?) but in practice you really want nothing. Somehow just having an order works, but it feels weird to me not to be able to factorise the max which is (almost) always going to be the same thing.

I'm asserting that you can have all the same things, just with less variables

If you want one Prop, you can have that, if you want a hierarchy you can have that too

you are just changing the domain of the quantification of the variables

if you had two hierarchies and wanted to say that `u`

is a Prop universe (which would normally show up as a use of `Prop i`

in the concrete syntax), this would be a variable `u`

plus a constraint `isProp(u)`

. This constraint is not an inequality constraint, it would be handled as its own thing

I agree, I just mean that the universe of a $\Pi$ type is now less uniform? It has to rely on the *rules* of a PTS right?

in the case of Coq's actual universe hierarchy there is only one such constraint you need, namely `isType(u)`

What even is the universe of a pi type in 8.20 sort polymorphic world?

Whereas if you separate the two you can say `forall (x : A), B`

has type `V (max i j)`

where `A : U i`

and `B : V j`

.

as with lean, the way to encode this is to have a function on universe variables with the definition you want

we may as well have named `imax`

as `theUniverseOfPi(u,v)`

Admittedly this is my own perspective on the matter, and this might not reflect what is implemented in Coq currently.

I think we agree, I'm just saying it seems to be more specialised with the two. But maybe that doesn't help in any way, with a bigger cost as you suggest.

Mario Carneiro said:

as with lean, the way to encode this is to have a function on universe variables with the definition you want

with cumulativity the definition on ground univs is not the only thing that matters, you also need to be able to handle constraints

well `imax`

doesn't just work on ground univs, it has normalization rules for open terms too

but a lot of the time it is just an expression which doesn't reduce

the "definition" I gave of the `imax`

function is only in the semantics, in reality it is implemented as a bunch of normalization rules consistent with that interpretation

Mario Carneiro said:

I don't see the advantage of having two different axes for a universe level. Why not have a variable which represents the pair? In fact, isn't that exactly what Coq used to do?

The main usability issue in that case is when one wants to share universe levels but not sorts, i.e. you'd have to write constraints like:

`foo@{u v | u.level = v.level) : (A : Type@{u}} {B : Type@{v}}, ...`

. The advantage would be that (Prop|SProp).level could be set to 0 however.

Same problem when you want to share the sort but not the levels (the more common case).

The forall typing rule would be `(forall (a : A : Type@{u}), B : Type@{v}) : Type@{(v.sort | max (u.level, v.level))}`

with (Prop, _) = (Prop, 0) presumably

I tried to advocate for trying that presentation but in the end the notational burden seems worst for "packed" universes

Last updated: Oct 13 2024 at 01:02 UTC