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

[effectfully]

> 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. For my use case type-in-type is slightly overkill, since
I want to disable universe checking only for the final (... : Set l
where) in a data definition (e.g. in the `call' constructor in
(lookupᶻ i Ψs (lookupᵐ i Rs) A R′) I want universes to be checked).
Though, I can live without the ability to disable universe checking
like that: those `Lift*'s are ugly, but work.

This hypothetical NO_UNIVERSE_CHECK pragma can be used like this:

    {-# NO_UNIVERSE_CHECK #-}
    Set₁′ : Set₃
    Set₁′ = Set₁

thus allowing some definitional cumulativity. Don't know whether this
is consistent with the current treatment of universes though. But it
should be OK for data types as they already allow cumulativity when it
is obvious.