------------------------------------------------------------------------ -- Universes ------------------------------------------------------------------------ {-# OPTIONS --universe-polymorphism #-} module Universe where open import Level -- Universes. record Universe u e : Set (suc (u ⊔ e)) where field -- Codes. U : Set u -- Decoding function. El : U → Set e