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