<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>&nbsp; &nbsp; ((i : Level) -&gt; Set i) -&gt; (i : Level) -&gt; 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; ">&nbsp; &nbsp; id : {i : Level} {A : Set i} -&gt; A -&gt; A</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; 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; ">&nbsp; &nbsp;&nbsp;</div><div style="color: rgb(0, 0, 0); font-size: 13px; font-family: arial, helvetica, sans-serif; background-color: transparent; font-style: normal; ">&nbsp; &nbsp; -- 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; ">&nbsp; &nbsp; id id : {i : Level} {A : Set i} -&gt; A -&gt; 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>&nbsp;</div><div>- darryl</div>  </div></body></html>