The Coq mailing list

["James Lottes" <jlottes AT gmail.com>]

The Type2le constant in your link is a great example, as it has a universe
parameter which isn't in the type or definition. I think there is a parallel
to be drawn with section variables. It's nice that Coq gives the user
mechanisms (Proof using) for explicitly controlling whether section variables
that are not used in a definition are included in the signature. It would be
nice if that were the case for universes too. I do think Type2le is rather
hackish; it looks to me like a clear use case for exposing access to a core
language with explicit universe parameters and constraints.

On the other side, I think there are also examples where one would like to
eliminate universe variables even when they appear in the type. Consider

Definition arrow A B := A -> B.
Definition arrow2 A B C := arrow A (arrow B C).
Definition arrow2' A B C := A -> B -> C.

arrow2 and arrow2' are convertible here, but arrow2 has an extra universe
parameter, and it appears in the type. This is an example where a transparent
constant (arrow) does not behave exactly transparently. You pay a price in
extra universe variables for using the abstraction. It would be nice if this
extra parameter could be eliminated by either instantiating it with an
algebraic universe, or wrapping it up in an existential package somehow. But
here the issues in the metatheory get complicated, and I don't know if this
could be made to work. It's clear, for example, that given universe
constraints i < j < k,  we cannot eliminate the middle parameter and still
have a conjunction of atomic constraints. I am more optimistic that some
workable metatheory could be found in which universe parameters unbounded
above could always be eliminated. Ideally, one would be able to both
explicitly add and remove universe parameters, and there would be some
sensible defaults.

I focused on the case of opaque terms before, because I thought the behavior I
suggested is a reasonable default in that case, and moreover shouldn't require
significant effort in either the metatheory or the code. Unfortunately, it
sounds like it wouldn't help with the 2000 universe definition in HoTT. I
faced something like this myself; after going back to carefully constrain the
universe sets I saw a reduction in a compiled file size from 15MB to .5MB, and
a huge boost in performance as well.