[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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$
