------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed universes
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Universe.Indexed where

open import Data.Product
open import Data.Universe
open import Function
open import Level

------------------------------------------------------------------------
-- Definitions

record IndexedUniverse i u e : Set (suc (i ⊔ u ⊔ e)) where
  field
    I  : Set i                 -- Index set.
    U  : I → Set u             -- Codes.
    El : ∀ {i} → U i → Set e   -- Decoding function.

  -- An indexed universe can be turned into an unindexed one.

  unindexed-universe : Universe (i ⊔ u) e
  unindexed-universe = record
    { U  = ∃ λ i → U i
    ; El = El ∘ proj₂
    }