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

[Andrés Sicard-Ramírez]

On 29 December 2015 at 23:00, effectfully <effectfully at gmail.com> wrote:
>> I created a branch allowing type in type and universe polymorphism.
>
> I tried it, but I'm using Agda 2.5 and my code doesn't typecheck with
> Agda 2.4.2.6.

You can try the issue-1764-master branch:

  $ git clone https://github.com/agda/agda.git
  $ cd agda
  $ git checkout issue-1764-master
  $ make install-bin

-- 
Andrés