/usr/share/agda-stdlib/Universe.agda is in agda-stdlib 0.6-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Universes
------------------------------------------------------------------------
module Universe where
open import Data.Product
open import Function
open import Level
-- Universes.
record Universe u e : Set (suc (u ⊔ e)) where
field
-- Codes.
U : Set u
-- Decoding function.
El : U → Set e
-- Indexed universes.
record Indexed-universe i u e : Set (suc (i ⊔ u ⊔ e)) where
field
-- Index set.
I : Set i
-- Codes.
U : I → Set u
-- Decoding function.
El : ∀ {i} → U i → Set e
-- 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₂
}
|