<html><body><div style="color:#000; background-color:#fff; font-family:arial, helvetica, sans-serif;font-size:10pt"><div><span>Using type judgments like this suggests that there should be ways to have universe polymorphism but also allow "obnoxiously large" 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) -> Set i) -> (i : Level) -> Set i</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; ">but wouldn't allow something like this:</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> id : {i : Level} {A : Set i} -> A -> A</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> id x = x</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> </div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> -- this should
fail</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "> id id : {i : Level} {A : Set i} -> A -> A</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; "><br></div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">because you can't get the judgment that the type of id is a Set i for some i, all you can get is that it's a type. is it then impossible to give id a type so that self application is possible, without yielding some form of inconsistency?</div><div></div><div> </div><div>- darryl</div> </div></body></html>