Stream: Coq users

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


view this post on Zulip 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}

view this post on Zulip 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.

view this post on Zulip Matthieu Sozeau (Dec 08 2020 at 15:19):

Yep, not yet!

view this post on Zulip Théo Winterhalter (Dec 08 2020 at 15:25):

Ok thanks!


Last updated: Jan 29 2023 at 01:02 UTC