[Agda] Universe Hierarchy Problem?

[kahl at cas.mcmaster.ca]

Andreas Abel answered my question about universe subtyping documentation:

 > >> To me, that seems to indicate the claim that Set is not a subtype of
 > >> Set1, [...]
 > >
 > > Set is not a subtype of Set₁.
 > 
 > 
 > In Ulf's thesis I read (p. 72)
 > 
 > 3.7.3 Universe hierarchy
 > In the presence of a universe hierarchy the logic has to be extended  
 > by level
 > metavariables. This is because when we instantiate a metavariable with
 > a function type as described above, we do not know what levels the new
 > metavariables should live at. It is unclear at this point how to  
 > handle the interaction between universe subtyping and level
 > metavariables, since this will introduce inequality constraints between
 > the variables, rather than equality constraints. The current
 > implementation turns unsolved inequalities into equality constraints,
 > which will necessarily exclude valid solutions.
 >
 > [...]

Thanks!

For now, I am trying out universe polymorphism, and enjoying that ---
I guess once universe polymorphism enters the reference manual,
the whole situation will be described more precisely
at a place that is more easily found...

(What is the general attitude towards the reference manual wiki pages?
 Some of it feels more like a tutorial than a reference document.
)


Wolfram