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

[effectfully]

Andreas Abel, thanks, I reported a bug.

Is it possible to make this

>One way to implement this is that whenever we conversion-check Set l ?= Set l' and we have --type-in-type, we set a flag in the type-checking environment that we want to ignore all errors coming from the comparison of the levels l ?= l'.

work not for a whole file, but for a particular level? Something like

t : Set (trusted α)
t = Set β

and `t' is treated as (t : Set α) everywhere outside the definition of `t'?