Consider a basic wrapper for a type with some arbitrary extra requirement:

```
Set Printing Universes.
Polymorphic Cumulative Record TypeWrapper@{u} := {
WrapT: Type@{u};
}.
(* TypeWrapper@{u} : Type@{u+1}
(* +u |= *) *)
```

When we define it to be universe polymorphic, the universe parameter `u`

is covariant, which is no surprise since we can legitimately convert the wrapped type to a Type in a higher universe, but not the other way around.

However, as soon as I use the wrapped type in an inductive:

```
Polymorphic Cumulative Inductive ValueWrapper@{u} (t: TypeWrapper@{u}) :=
| WrapV (v: WrapT t).
(* ValueWrapper@{u} : TypeWrapper@{u} -> Type@{u}
(* =u |= *) *)
```

the universe parameter becomes invariant, and I fail to see how having covariant `u`

would break the universe hierarchy. By contrast, using a parameter `(t: Type@{u})`

with `WrapV (v: t)`

makes `u`

irrelevant.

- Is there any documentation on how all of this works (I'm pretty sure there isn't but who knows)?
- Where do the covariant/irrelevant outputs for my examples come from?
- Is there a clean way to convert a
`ValueWrapper@{u}`

to a higher universe`v`

when`t`

itself can be converted to a`TypeWrapper@{v}`

? (Maybe with explicit lifting?)

the cumulativity of `Ind@{u1 ... un}`

is determined by comparing the constructor argument types of `Ind@{u1 ... un}`

with the ones at a different instances ie the ones of `Ind@{u1' ... un'}`

: `C_i@{u1 ... un} <= C_i@{u1' ... un'}`

additionally the same is done for the indices telescope, and the indices arguments in the return types of the constructors must be convertible (`=`

not `<=`

) (this doesn't matter for records since there are no indices)

if `uj = uj'`

is required then `uj`

is invariant

if `uj <= uj'`

is required then `uj`

is covariant

otherwise `uj`

is irrelevant

`WrapT@{u} t`

expands to `match t return Type@{u} with Build_TypeWrapper x => x end`

because of the `return Type@{u}`

, `WrapT@{u} t <= WrapT@{v} t`

implies `u = v`

so the universe is invariant

In this case you could use primitive projections, if `TypeWrapper`

is primitive then `WrapT t`

is normal form and does not mention any universe.

Thanks @Gaëtan Gilbert. Primitive projections did solve that issue, avoiding (if I understand correctly) a call to the projection function and thus associated constraints. It took me a while to propagate this change (I've got like 5k lines impacted :sweat_smile: ) but I'm pretty sure now the issues I have left are unrelated.

Last updated: Jun 23 2024 at 05:02 UTC