Explicit Sort hierarchy

[be5invis]

Status quo:

Prop : Type
Prop = Type

Looks better:

Prop : Type_1
Prop = Type

[ahmadsalim]

@be5invis Could you kindly provide a deeper rationale for why you need this explicit sort hierarchy?

[be5invis]

Don’t you think

Prop : Type
Prop = Type

is weird?

[ahmadsalim]

@be5invis I do not, in fact I think the opposite is weird :).

Sorry, but I will close this issue since I think it would require a lot of work to add explicit levels without a very small benefit and so I would think there is an abysmal chance of this getting implemented.