[Agda] Is it possible to switch off universes checking?

Andrés Sicard-Ramírez asr at eafit.edu.co
Wed Dec 30 04:04:52 CET 2015


On 29 December 2015 at 20:19, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> Question: which type theory do you claim to implement with this?

I don't know.

(Ulf added the incompatibility of using type in type and universe
polymorphism. Maybe he had a good reason for it.)

-- 
Andrés


More information about the Agda mailing list