|
431
|
1 open import Level
|
|
|
2 open import Ordinals
|
|
|
3 module VL {n : Level } (O : Ordinals {n}) where
|
|
|
4
|
|
|
5 open import zf
|
|
|
6 open import logic
|
|
|
7 import OD
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import Relation.Binary
|
|
|
10 open import Data.Empty
|
|
|
11 open import Relation.Binary
|
|
|
12 open import Relation.Binary.Core
|
|
|
13 open import Relation.Binary.PropositionalEquality
|
|
|
14 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
15 import BAlgbra
|
|
|
16 open BAlgbra O
|
|
|
17 open inOrdinal O
|
|
|
18 import OrdUtil
|
|
|
19 import ODUtil
|
|
|
20 open Ordinals.Ordinals O
|
|
|
21 open Ordinals.IsOrdinals isOrdinal
|
|
|
22 open Ordinals.IsNext isNext
|
|
|
23 open OrdUtil O
|
|
|
24 open ODUtil O
|
|
|
25
|
|
|
26 open OD O
|
|
|
27 open OD.OD
|
|
|
28 open ODAxiom odAxiom
|
|
|
29 -- import ODC
|
|
|
30 open _∧_
|
|
|
31 open _∨_
|
|
|
32 open Bool
|
|
|
33 open HOD
|
|
|
34
|
|
|
35 -- The cumulative hierarchy
|
|
|
36 -- V 0 := ∅
|
|
|
37 -- V α + 1 := P ( V α )
|
|
|
38 -- V α := ⋃ { V β | β < α }
|
|
|
39
|
|
|
40 V : ( β : Ordinal ) → HOD
|
|
|
41 V β = TransFinite V1 β where
|
|
|
42 V1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
43 V1 x V0 with trio< x o∅
|
|
|
44 V1 x V0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
45 V1 x V0 | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
46 V1 x V0 | tri> ¬a ¬b c with Oprev-p x
|
|
|
47 V1 x V0 | tri> ¬a ¬b c | yes p = Power ( V0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
48 V1 x V0 | tri> ¬a ¬b c | no ¬p =
|
|
|
49 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (V0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
50
|
|
|
51 --
|
|
|
52 -- L ⊆ HOD ⊆ V
|
|
|
53 --
|
|
|
54 -- HOD=V : (x : HOD) → V (odmax x) ∋ x
|
|
|
55 -- HOD=V x = {!!}
|
|
|
56
|
|
|
57 --
|
|
|
58 -- Definition for Power Set
|
|
|
59 --
|
|
|
60 record Definitions : Set (suc n) where
|
|
|
61 field
|
|
|
62 Definition : HOD → HOD
|
|
|
63
|
|
|
64 open Definitions
|
|
|
65
|
|
|
66 Df : Definitions → (x : HOD) → HOD
|
|
|
67 Df D x = Power x ∩ Definition D x
|
|
|
68
|
|
|
69 -- The constructible Sets
|
|
|
70 -- L 0 := ∅
|
|
|
71 -- L α + 1 := Df (L α) -- Definable Power Set
|
|
|
72 -- V α := ⋃ { L β | β < α }
|
|
|
73
|
|
|
74 L : ( β : Ordinal ) → Definitions → HOD
|
|
|
75 L β D = TransFinite L1 β where
|
|
|
76 L1 : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
77 L1 x L0 with trio< x o∅
|
|
|
78 L1 x L0 | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
79 L1 x L0 | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
80 L1 x L0 | tri> ¬a ¬b c with Oprev-p x
|
|
|
81 L1 x L0 | tri> ¬a ¬b c | yes p = Df D ( L0 (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
82 L1 x L0 | tri> ¬a ¬b c | no ¬p =
|
|
|
83 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (L0 y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
84
|
|
|
85 V=L0 : Set (suc n)
|
|
|
86 V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
|
