------------------------------------------------------------------------
-- The Agda standard library
--
-- Universes
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Universe where

open import Level

------------------------------------------------------------------------
-- Definition

record Universe u e : Set (suc (u ⊔ e)) where
  field
    U : Set u       -- Codes.
    El : U → Set e  -- Decoding function.