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

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

module Data.Universe.Indexed where

open import Data.Product.Base using (∃; proj₂)
open import Data.Universe using (Universe)
open import Function.Base using (_∘_)
open import Level using (Level; _⊔_; suc)

------------------------------------------------------------------------
-- 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₂
    }