[Agda] Re: Builtins

[Jesper Cockx]

The type theory used in the paper uses a simple hierarchy of fixed
universes Set0, Set1, ... 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:
http://www.pps.univ-paris-diderot.fr/~sozeau/research/publications/Universe_Polymorphism_in_Coq.pdf

Jesper

On Mon, Apr 27, 2015 at 9:27 AM, N. Raghavendra <raghu at hri.res.in> wrote:

> At 2015-04-26T10:41:53+02:00, Jesper Cockx wrote:
>
> > In fact, our ICFP '14 paper gives exactly such a guarantee. So if
> > anything in Agda allows you to prove K with --without-K enabled, it's
> > probably a bug in the implementation. If you are interested in the
> > subject, you can read the paper here: https://lirias.kuleuven.be/
> > bitstream/123456789/452283/2/icfp14-cockxA.pdf
>
> Thanks for the clarification, and for the link!  I'd somehow downloaded
> a two-page version of your paper earlier, and with my lack of background
> in type theory that wasn't very instructive, but this longer version is
> quite useful, especially the introduction and the formal statement of
> Agda's type theory in Figure 2.
>
> I want to ask something about the latter.  There is no rule for deriving
> judgements involving the type Level in Figure 2.  Is Level considered a
> "defined" type like Σ, as opposed to a "core" type such as (x : A) → B?
> Also, are you taking the same definition of "term" as in the reference
> manual,
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.CoreSyntax
> ?
> What is the role of literals in that syntax?
>
> Thanks and cheers,
> Raghu.
>
> --
> N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
> Harish-Chandra Research Institute, http://www.hri.res.in/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150427/839cf738/attachment.html