<p dir="ltr">I forgot to mention what Agda's Setomega means. I'm not familiar with Agda's source code, so I'm mainly guessing.</p>
<p dir="ltr">In Agda there is only one judgement "a : A", but there is a special thing called Setomega whose only possible use is at the right-hand side of a colon, and the judgement "A : Setomega" in Agda means exactly the same thing as my judgement "A type".<br>
Setomega is not a valid term and not even a valid type, you cannot consider Setomega -> Setomega for instance. The only use of Setomega is to embed easily the judgment "A type" in Agda's source code where everything was supposed to have a type before the introduction of universe polymorphisn.</p>
<p dir="ltr">Guillaume</p>
<div class="gmail_quote">Le 30 juin 2013 15:54, "Guillaume Brunerie" <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> a écrit :<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<p dir="ltr">I will describe a type theory with infinitely many universes (à la Russel), and explicit universe polymorphism with a type of universe level (this is basically what Agda does)</p>
<p dir="ltr">There are two basic judgments:</p>
<p dir="ltr">A type<br>
a : A</p>
<p dir="ltr">Note that unlike in Coq, the first judgment is not a special case of the second one, a valid type need not be a valid term.<br>
The possible expressions are the following:</p>
<p dir="ltr">Level, zero, succ, max, Set i,<br>
(x : A) -> B(x), lambda x -> u(x), u v</p>
<p dir="ltr">The typing rules are the following</p>
<p dir="ltr">* Universe levels:</p>
<p dir="ltr">Level : Set zero<br>
zero : Level<br>
succ : Level -> Level<br>
max : Level -> Level -> Level</p>
<p dir="ltr">* Universes:</p>
<p dir="ltr">i : Level<br>
----------<br>
Set i : Set (succ i)</p>
<p dir="ltr">A : Set i<br>
----------<br>
A type</p>
<p dir="ltr">A : Set i<br>
---------- (cumulativity, optional, not present in Agda)<br>
A : Set (succ i)</p>
<p dir="ltr">* Pi formation (there are two formation rules, one for arbitrary types and one for small types):</p>
<p dir="ltr">A type<br>
x : A |- B(x) type<br>
----------<br>
(x : A) -> B(x) type</p>
<p dir="ltr">i j : Level<br>
A : Set i<br>
x : A |- B(x) : Set j<br>
----------<br>
(x : A) -> B(x) : Set (max i j)</p>
<p dir="ltr">* Pi introduction, elimination and computation:</p>
<p dir="ltr">As usual (and (x : A) -> B(x) is not required to small)</p>
<p dir="ltr">*****</p>
<p dir="ltr">For the transfinite version, you replace "Level : Set zero" by "Level type", change max to sup with the appropriate typing rule and change the second Pi formation rule by one where j can depend on x and where the universe level is computed with sup.</p>
<p dir="ltr">Note that (in the first version) in order to have a small Pi-type, the codomain is required to be of a uniform universe level, in particular a valid type like (i : Level) -> Set i is not a valid term.<br>
In the transfinite version, this requirement is dropped, any Pi between small types is small even if the codomain is not of a uniform universe level. But on the other hand the type of universe levels is now big, so (i : Level) -> Set i is still not a valid term (and still a valid type).<br>
And in the transfinite version, (n : Nat) -> Set (Nat-to-Level n) is small and of type Set omega (and you can define Nat-to-Level because you have large elimination), but it's big in the first version.</p>
<p dir="ltr">I also already sketched the set-theoretic semantics of both versions in some previous email, so it seems consistent.</p>
<p dir="ltr">Best,<br>
Guillaume</p>
<div class="gmail_quote">Le 30 juin 2013 14:02, "Darryl McAdams" <<a href="mailto:psygnisfive@yahoo.com" target="_blank">psygnisfive@yahoo.com</a>> a écrit :<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div><div style="font-size:10pt;font-family:arial,helvetica,sans-serif"><div><span>It was mentioned in the referenced thread that types like</span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<span><br></span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif"><span> {i : Level} -> {A : Set l} -> A -> A</span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">
<span><br></span></div><div style="font-style:normal;font-size:13px;background-color:transparent;font-family:arial,helvetica,sans-serif">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></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div>
</blockquote></div>