------------------------------------------------------------------------
-- 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₂
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4