Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison ordinal-definable.agda @ 29:fce60b99dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
posturate OD is isomorphic to Ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 May 2019 18:18:43 +0900
parents constructible-set.agda@f36e40d5d2c3
children 3b0fdb95618e
comparison
equal deleted inserted replaced
28:f36e40d5d2c3 29:fce60b99dc55
1 open import Level
2 module ordinal-definable where
3
4 open import zf
5 open import ordinal
6
7 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
8
9 open import Relation.Binary.PropositionalEquality
10
11 open import Data.Nat.Properties
12 open import Data.Empty
13 open import Relation.Nullary
14
15 open import Relation.Binary
16 open import Relation.Binary.Core
17
18
19 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
20
21 -- Ordinal Definable Set
22
23 -- o∋ : {n : Level} → {A : Ordinal {n}} → (OrdinalDefinable {n} A ) → (x : Ordinal {n} ) → (x o< A) → Set n
24 -- o∋ a x x<A = def a x x<A
25
26 -- TC u : Transitive Closure of OD u
27 --
28 -- all elements of u or elements of elements of u, etc...
29 --
30 -- TC Zero = u
31 -- TC (suc n) = ∪ (TC n)
32 --
33 -- TC u = TC ω u = ∪ ( TC n ) n ∈ ω
34 --
35 -- u ∪ ( ∪ u ) ∪ ( ∪ (∪ u ) ) ....
36 --
37 -- Heritic Ordinal Definable
38 --
39 -- ( HOD = {x | TC x ⊆ OD } ) ⊆ OD x ∈ OD here
40 --
41
42 record OD {n : Level} : Set (suc n) where
43 field
44 def : (x : Ordinal {n} ) → Set n
45
46 open OD
47 open import Data.Unit
48
49 postulate
50 od→ord : {n : Level} → OD {n} → Ordinal {n}
51
52 ord→od : {n : Level} → Ordinal {n} → OD {n}
53 ord→od x = record { def = λ y → x ≡ y }
54
55 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
56 _∋_ {n} a x = def a ( od→ord x )
57
58 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
59 x c< a = a ∋ x
60
61 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n)
62 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
63
64 postulate
65 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord x
66 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od x
67 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
68 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
69 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
70 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ
71
72 HOD = OD
73
74 od∅ : {n : Level} → HOD {n}
75 od∅ {n} = record { def = λ _ → Lift n ⊥ }
76
77 ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} )
78 ∅1 {n} x (lift ())
79
80 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
81 HOD→ZF {n} = record {
82 ZFSet = OD {n}
83 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x )
84 ; _≈_ = _≡_
85 ; ∅ = od∅
86 ; _,_ = _,_
87 ; Union = Union
88 ; Power = Power
89 ; Select = Select
90 ; Replace = Replace
91 ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }
92 ; isZF = isZF
93 } where
94 Replace : OD {n} → (OD {n} → OD {n} ) → OD {n}
95 Replace X ψ = sup-od ψ
96 Select : OD {n} → (OD {n} → Set (suc n) ) → OD {n}
97 Select X ψ = record { def = λ x → select ( ord→od x ) } where
98 select : OD {n} → Set n
99 select x with ψ x
100 ... | t = Lift n ⊤
101 _,_ : OD {n} → OD {n} → OD {n}
102 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
103 Union : OD {n} → OD {n}
104 Union x = record { def = λ y → {z : Ordinal {n}} → def x z → def (ord→od z) y }
105 Power : OD {n} → OD {n}
106 Power x = record { def = λ y → (z : Ordinal {n} ) → ( def x y ∧ def (ord→od z) y ) }
107 ZFSet = OD {n}
108 _∈_ : ( A B : ZFSet ) → Set n
109 A ∈ B = B ∋ A
110 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set n
111 _⊆_ A B {x} = A ∋ x → B ∋ x
112 _∩_ : ( A B : ZFSet ) → ZFSet
113 A ∩ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∧ (Lift (suc n) ( B ∋ x ) ))
114 _∪_ : ( A B : ZFSet ) → ZFSet
115 A ∪ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∨ (Lift (suc n) ( B ∋ x ) ))
116 infixr 200 _∈_
117 infixr 230 _∩_ _∪_
118 infixr 220 _⊆_
119 isZF : IsZF (OD {n}) (λ a x → Lift (suc n) ( a ∋ x )) _≡_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } })
120 isZF = record {
121 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
122 ; pair = pair
123 ; union→ = {!!}
124 ; union← = {!!}
125 ; empty = empty
126 ; power→ = {!!}
127 ; power← = {!!}
128 ; extentionality = {!!}
129 ; minimul = {!!}
130 ; regularity = {!!}
131 ; infinity∅ = {!!}
132 ; infinity = {!!}
133 ; selection = {!!}
134 ; replacement = {!!}
135 } where
136 open _∧_
137 pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B)
138 proj1 (pair A B ) = lift ( case1 refl )
139 proj2 (pair A B ) = lift ( case2 refl )
140 empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x)
141 empty x (lift (lift ()))
142 union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y)
143 union→ X x y (lift X∋x) (lift x∋y) = lift lemma where
144 lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
145 lemma {z} X∋z = {!!}
146
147
148
149
150
151