Hello.

Consider the universe polymorphic version of the `unit`

inductive:

```
Inductive unit@{i} : Type@{i} := tt : unit.
```

Why are `L`

and `L1`

different in the following code?

```
sort (typ S) = {{ Set }},
coq.univ.variable S Uv,
coq.univ-instance UI [Uv],
coq.locate "unit" Unit,
coq.elaborate-skeleton (pglobal Unit UI) (sort (typ L)) _ ok,
coq.elaborate-skeleton (pglobal Unit UI) (sort (typ L1)) _ ok.
```

It is in the spec of elaboration, try `@keepunivs!`

or `coq.typecheck`

Thanks for the option suggestion. btw I think there was a reason why I started using `elaborate-skeleton`

also for typechecking rather than `typecheck`

, but cannot remember it.

The fresh variable generation goes on in the case of `Type`

, even with the option:

```
@keepunivs! => coq.elaborate-skeleton (sort (typ T)) Ty _ ok,
@keepunivs! => coq.elaborate-skeleton (sort (typ T)) Ty2 _ ok
```

```
T = «Test.941»
Ty = sort (typ «Test.943»)
Ty2 = sort (typ «Test.946»)
```

With `typecheck`

, I get the behaviour I expect (generating that `+1`

) only if I give a variable as output:

```
coq.typecheck (sort (typ T)) (sort (typ L)) ok,
coq.typecheck (sort (typ T)) A ok
```

```
L = «Test.948»
A = sort (typ «Test.941+1»)
```

keepunivs should change what you discard, try to print it.

About Ty and Ty2, they are variables you can force to be equal with the APIs

Is there any way to dodge the fresh universe creation with `coq.univ.variable`

? I can make all my typechecks give always the same value with the example I gave with `coq.typecheck`

and a variable as output, but `coq.univ.variable`

will keep creating a fresh universe variable each time. I'd like to have that `«Test.10+1»`

as a universe variable then as a universe instance, so that:

- my code doing substitutions with
`copy`

will syntactically match terms correctly (if universe instances don't match it does not work); - when giving the final term to
`coq.env.add-const`

it will not add extra binders to the universe instance.

I'd need more time to investigate, but I have the feeling it is the code to purge algebraics that bothers you. Would you try switching it off?

I think I did that already in my local version of Coq-Elpi

`coq.univ.variable`

runs into this branch, which calls this auxiliary function. Then as the universe is not a named level but some algebraic stuff (something +1), it takes the `None`

branch and `new_univ_blahblahblah`

I guess we need to do a visio session next week, this way it will be faster

ok maybe I can use `Sorts.super`

to model that +1 directly in the variable

Last updated: Apr 21 2024 at 01:02 UTC