[TYPES] Giving semantics to universes with explicit universe polymorphism

[Jason Hu]

Hi all,

I am working on a system with explicit universe polymorphism similar to Agda, a la Bezem et al. [1], with non-cumulative, Tarski-style universes. When I try to give a semantics to types and universes a la Abel et al.[2], it does not seem obvious to me how universe polymorphism should be captured. In particular, I am not sure how do we say "the semantics is coherent with substitutions with universe variables", or more technically, how the semantics of U(l) should be assigned where l is a universe variable, so that the semantics of U(k) is obtained given a substitution k/l for some well-formed universe level k?

Any pointer is appreciated.

[1] https://urldefense.com/v3/__https://arxiv.org/pdf/2212.03284.pdf__;!!IBzWLUs!UinFJQgLg436Sh8FIzlYlW8J6QXsm-6HH76jzOp4LAvCDJZQXoo9r7rotdf3cwM8wpB10MSKNPSAuDHoTOV3R0JquvdDUHM$ 
[2] https://urldefense.com/v3/__https://www2.tcs.ifi.lmu.de/*abel/popl18.pdf__;fg!!IBzWLUs!UinFJQgLg436Sh8FIzlYlW8J6QXsm-6HH76jzOp4LAvCDJZQXoo9r7rotdf3cwM8wpB10MSKNPSAuDHoTOV3R0JqqdRFqVc$ 

Thanks,
Jason Hu
https://urldefense.com/v3/__https://hustmphrrr.github.io/__;!!IBzWLUs!UinFJQgLg436Sh8FIzlYlW8J6QXsm-6HH76jzOp4LAvCDJZQXoo9r7rotdf3cwM8wpB10MSKNPSAuDHoTOV3R0JqAFBpv1o$