<div dir="ltr"><div>The type theory used in the paper uses a simple hierarchy of fixed universes Set<sub>0</sub>, Set<sub>1</sub>, ... and doesn't support universe polymorphism. In other words, it doesn't have a Level type. It wouldn't be hard to add a primitive type Level with terms zero : Level, suc: Level → Level, and max : Level → Level → Level and corresponding expressions Set l : Set (suc l) for l : Level, though the corresponding extra typing rules needed would take up some more space. Here is a paper from last year about the same subject in Coq: <a href="http://www.pps.univ-paris-diderot.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf">http://www.pps.univ-paris-diderot.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf</a><br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Apr 27, 2015 at 9:27 AM, N. Raghavendra <span dir="ltr"><<a href="mailto:raghu@hri.res.in" target="_blank">raghu@hri.res.in</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">At 2015-04-26T10:41:53+02:00, Jesper Cockx wrote:<br>
<br>
> In fact, our ICFP '14 paper gives exactly such a guarantee. So if<br>
> anything in Agda allows you to prove K with --without-K enabled, it's<br>
> probably a bug in the implementation. If you are interested in the<br>
> subject, you can read the paper here: <a href="https://lirias.kuleuven.be/" target="_blank">https://lirias.kuleuven.be/</a><br>
> bitstream/123456789/452283/2/icfp14-cockxA.pdf<br>
<br>
</span>Thanks for the clarification, and for the link! I'd somehow downloaded<br>
a two-page version of your paper earlier, and with my lack of background<br>
in type theory that wasn't very instructive, but this longer version is<br>
quite useful, especially the introduction and the formal statement of<br>
Agda's type theory in Figure 2.<br>
<br>
I want to ask something about the latter. There is no rule for deriving<br>
judgements involving the type Level in Figure 2. Is Level considered a<br>
"defined" type like Σ, as opposed to a "core" type such as (x : A) → B?<br>
Also, are you taking the same definition of "term" as in the reference<br>
manual,<br>
<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.CoreSyntax" target="_blank">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.CoreSyntax</a>?<br>
What is the role of literals in that syntax?<br>
<div class="HOEnZb"><div class="h5"><br>
Thanks and cheers,<br>
Raghu.<br>
<br>
--<br>
N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>>, <a href="http://www.retrotexts.net/" target="_blank">http://www.retrotexts.net/</a><br>
Harish-Chandra Research Institute, <a href="http://www.hri.res.in/" target="_blank">http://www.hri.res.in/</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">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>
</div></div></blockquote></div><br></div>