Primitive.agda [was [Agda-dev] Agda and Packages/Libraries]

[Ulf Norell]

On Mon, Feb 15, 2016 at 3:14 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
wrote:

> On 15 February 2016 at 08:37, Ulf Norell <ulf.norell at gmail.com> wrote:
> > Clearly Agda.Primitive ought to be considered safe. Or is universe
> > polymorphism not in the safe fragment?
>
> Strictly speaking, Primitve.Agda isn't using universe polymorphism.


No, but universe polymorphism requires builtin levels which need postulates.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20160215/c3d51f2b/attachment.html