Stream: Coq users

Topic: Explicit universe levels turn j > i into i+1

Théo Winterhalter (Dec 08 2020 at 11:13):

Hi, when using explicit universe levels we can use algebraic in some cases (like in the type of an inductive type) but is it possible to use it in the type of definitions?
In particular I have some function

foo@{i j} : Type@{i} -> Type@{j}
(* i j ||= i < j *)

and I'm wondering if I can turn it into

foo@{i} : Type@{i} -> Type@{i+1}

Théo Winterhalter (Dec 08 2020 at 15:06):

ping @Matthieu Sozeau ?
I guess the answer is that what I want to do is not possible.

Matthieu Sozeau (Dec 08 2020 at 15:19):

Yep, not yet!

Théo Winterhalter (Dec 08 2020 at 15:25):

Ok thanks!

Last updated: Sep 30 2023 at 06:01 UTC