<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>It was mentioned in the referenced thread that types like</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span> {i : Level} -> {A : Set l} -> A -> A</span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><span><br></span></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">do not themselves have types. Even with transfinite levels it
couldn't be typed, because i would be instantiated to any level, including transfinite ones. How does level polymorphism get handled in a consistent type theory, if at all? Not just Agda's underlying type theory, but any type theory in general?</div><div></div><div> </div><div>- Darryl McAdams</div> </div></body></html>