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

[effectfully]

Nils Anders Danielsson, thanks, it worked.

Ulf Norell, your code typechecks. Moreover both

    ok : Set
    ok = id Set

and

    ok : Set₁
    ok = id Set

typecheck without unresolved metas.

This

    data D α β : Set β where
      C : Set α -> D α β

is OK too.

However

    data D {α} (A : Set α) : Set where
      C : A -> D A

results in

    Set != Set α
    when checking the constructor C in the declaration of D

Andrés Sicard-Ramírez, thanks for your effort.