|
1476
|
1 {-# OPTIONS --cubical-compatible --safe #-}
|
|
|
2 open import Level
|
|
|
3 open import Ordinals
|
|
|
4 open import logic
|
|
|
5 open import Relation.Nullary
|
|
|
6
|
|
431
|
7 open import Level
|
|
|
8 open import Ordinals
|
|
1476
|
9 import HODBase
|
|
|
10 import OD
|
|
|
11 open import Relation.Nullary
|
|
|
12 module VL {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where
|
|
|
13
|
|
|
14 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
15 open import Data.Empty
|
|
|
16
|
|
|
17 import OrdUtil
|
|
|
18
|
|
|
19 open Ordinals.Ordinals O
|
|
|
20 open Ordinals.IsOrdinals isOrdinal
|
|
|
21 import ODUtil
|
|
431
|
22
|
|
|
23 open import logic
|
|
1476
|
24 open import nat
|
|
|
25
|
|
431
|
26 open OrdUtil O
|
|
1476
|
27 open ODUtil O HODAxiom ho<
|
|
431
|
28
|
|
|
29 open _∧_
|
|
|
30 open _∨_
|
|
|
31 open Bool
|
|
1476
|
32
|
|
|
33 open HODBase._==_
|
|
|
34
|
|
|
35 open HODBase.ODAxiom HODAxiom
|
|
|
36 open OD O HODAxiom
|
|
|
37
|
|
|
38 open HODBase.HOD
|
|
|
39
|
|
|
40
|
|
|
41 open import Relation.Nullary
|
|
|
42 open import Relation.Binary
|
|
|
43 open import Data.Empty
|
|
|
44 open import Relation.Binary
|
|
|
45 open import Relation.Binary.Core
|
|
|
46 open import Relation.Binary.PropositionalEquality
|
|
|
47 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
48
|
|
431
|
49
|
|
|
50 -- The cumulative hierarchy
|
|
|
51 -- V 0 := ∅
|
|
|
52 -- V α + 1 := P ( V α )
|
|
|
53 -- V α := ⋃ { V β | β < α }
|
|
|
54
|
|
1458
|
55 V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
56 V1 x V0 with trio< x o∅
|
|
|
57 V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
58 V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
59 V1 x V0 | tri> ¬a ¬b c with Oprev-p x
|
|
|
60 V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
61 V1 x V0 | tri> ¬a ¬b c | no ¬p =
|
|
|
62 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
431
|
63
|
|
1458
|
64 record VOrd (x : Ordinal) : Set n where
|
|
|
65 field
|
|
|
66 β : Ordinal
|
|
|
67 ov : odef (TransFinite V1 β) x
|
|
431
|
68
|
|
1458
|
69 V : OD
|
|
|
70 V = record { def = λ x → VOrd x }
|
|
431
|
71
|
|
1458
|
72 record Vn : Set n where
|
|
|
73 field
|
|
|
74 x : Ordinal
|
|
|
75 β : Ordinal
|
|
|
76 ov : odef (TransFinite V1 β) x
|
|
431
|
77
|
|
1476
|
78 -- Vn∅ : Vn
|
|
|
79 -- Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
|
|
431
|
80
|
|
1476
|
81 -- vsuc : Vn → Vn
|
|
|
82 -- vsuc v = ?
|
|
431
|
83
|
|
1476
|
84 -- v< : Vn → Vn → Set n
|
|
|
85 -- v< x y = ?
|
|
1458
|
86
|
|
1476
|
87 -- IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
|
|
|
88 -- IsVOrd = ?
|
|
1458
|
89
|
