|
414
|
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 open OD O
|
|
|
19 open OD.OD
|
|
|
20 open ODAxiom odAxiom
|
|
|
21 -- import ODC
|
|
|
22 open _∧_
|
|
|
23 open _∨_
|
|
|
24 open Bool
|
|
|
25 open HOD
|
|
|
26
|
|
|
27 -- The cumulative hierarchy
|
|
415
|
28 -- V 0 := ∅
|
|
|
29 -- V α + 1 := P ( V α )
|
|
|
30 -- V α := ⋃ { V β | β < α }
|
|
414
|
31
|
|
|
32 V : ( β : Ordinal ) → HOD
|
|
|
33 V β = TransFinite1 Vβ₁ β where
|
|
|
34 Vβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
35 Vβ₁ x Vβ₀ with trio< x o∅
|
|
|
36 Vβ₁ x Vβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
415
|
37 Vβ₁ x Vβ₀ | tri≈ ¬a refl ¬c = Ord o∅
|
|
414
|
38 Vβ₁ x Vβ₀ | tri> ¬a ¬b c with Oprev-p x
|
|
|
39 Vβ₁ x Vβ₀ | tri> ¬a ¬b c | yes p = Power ( Vβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
415
|
40 Vβ₁ x Vβ₀ | tri> ¬a ¬b c | no ¬p =
|
|
|
41 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (Vβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
42
|
|
|
43 --
|
|
|
44 -- Definition for Power Set
|
|
|
45 --
|
|
|
46 record Definitions : Set (suc n) where
|
|
|
47 field
|
|
|
48 Definition : HOD → HOD
|
|
|
49
|
|
|
50 open Definitions
|
|
|
51
|
|
|
52 Df : Definitions → (x : HOD) → HOD
|
|
|
53 Df D x = Power x ∩ Definition D x
|
|
|
54
|
|
|
55 -- The constructible Sets
|
|
|
56 -- L 0 := ∅
|
|
|
57 -- L α + 1 := Df (L α) -- Definable Power Set
|
|
|
58 -- V α := ⋃ { L β | β < α }
|
|
|
59
|
|
|
60 L : ( β : Ordinal ) → Definitions → HOD
|
|
|
61 L β D = TransFinite1 Lβ₁ β where
|
|
|
62 Lβ₁ : (x : Ordinal ) → ( ( y : Ordinal) → y o< x → HOD ) → HOD
|
|
|
63 Lβ₁ x Lβ₀ with trio< x o∅
|
|
|
64 Lβ₁ x Lβ₀ | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a)
|
|
|
65 Lβ₁ x Lβ₀ | tri≈ ¬a refl ¬c = Ord o∅
|
|
|
66 Lβ₁ x Lβ₀ | tri> ¬a ¬b c with Oprev-p x
|
|
|
67 Lβ₁ x Lβ₀ | tri> ¬a ¬b c | yes p = Df D ( Lβ₀ (Oprev.oprev p ) (subst (λ k → _ o< k) (Oprev.oprev=x p) <-osuc ))
|
|
|
68 Lβ₁ x Lβ₀ | tri> ¬a ¬b c | no ¬p =
|
|
|
69 record { od = record { def = λ y → (y o< x ) ∧ ((lt : y o< x ) → odef (Lβ₀ y lt) x ) } ; odmax = x; <odmax = λ {x} lt → proj1 lt }
|
|
|
70
|
|
|
71 V=L0 : Set (suc n)
|
|
|
72 V=L0 = (x : Ordinal) → V x ≡ L x record { Definition = λ y → y }
|
