[Agda] Re: Builtins

[N. Raghavendra]

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/