Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal-definable.agda @ 43:0d9b9db14361
equalitu and internal parametorisity
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 24 May 2019 22:22:16 +0900 |
parents | 4d5fc6381546 |
children | fcac01485f32 |
comparison
equal
deleted
inserted
replaced
42:4d5fc6381546 | 43:0d9b9db14361 |
---|---|
31 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n | 31 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n |
32 _∋_ {n} a x = def a ( od→ord x ) | 32 _∋_ {n} a x = def a ( od→ord x ) |
33 | 33 |
34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n | 34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n |
35 x c< a = a ∋ x | 35 x c< a = a ∋ x |
36 | |
37 -- _=='_ : {n : Level} → Set (suc n) -- Rel (OD {n}) (suc n) | |
38 -- _=='_ {n} = ( a b : OD {n} ) → ( ∀ { x : OD {n} } → a ∋ x → b ∋ x ) ∧ ( ∀ { x : OD {n} } → a ∋ x → b ∋ x ) | |
39 | |
40 record _==_ {n : Level} ( a b : OD {n} ) : Set n where | |
41 field | |
42 eq→ : ∀ { x : Ordinal {n} } → def a x → def b x | |
43 eq← : ∀ { x : Ordinal {n} } → def b x → def a x | |
44 | |
45 id : {n : Level} {A : Set n} → A → A | |
46 id x = x | |
47 | |
48 eq-refl : {n : Level} { x : OD {n} } → x == x | |
49 eq-refl {n} {x} = record { eq→ = id ; eq← = id } | |
50 | |
51 open _==_ | |
52 | |
53 eq-sym : {n : Level} { x y : OD {n} } → x == y → y == x | |
54 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } | |
55 | |
56 eq-trans : {n : Level} { x y z : OD {n} } → x == y → y == z → x == z | |
57 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } | |
36 | 58 |
37 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) | 59 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) |
38 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) | 60 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) |
39 | 61 |
40 od∅ : {n : Level} → OD {n} | 62 od∅ : {n : Level} → OD {n} |
134 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅ | 156 -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅ |
135 -- ∅10 {n} x not = ? | 157 -- ∅10 {n} x not = ? |
136 | 158 |
137 open Ordinal | 159 open Ordinal |
138 | 160 |
139 ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y | 161 -- ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y |
140 ∋-subst refl refl x = x | 162 -- ∋-subst refl refl x = x |
141 | 163 |
142 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) | 164 -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) |
143 -- ∅77 {n} x lt = {!!} where | 165 -- ∅77 {n} x lt = {!!} where |
144 | 166 |
145 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} | 167 ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} |
146 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where | 168 ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where |
147 | 169 |
148 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x ≡ od∅ {n} | 170 ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n} |
149 ∅7 {n} x eq = trans ( trans (sym oiso)( cong ( λ k → ord→od k ) eq ) ) ∅7' | 171 ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where |
150 | 172 e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y |
151 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x ≡ od∅ → o∅ o< od→ord x | 173 e0 {y} (case1 ()) |
174 e0 {y} (case2 ()) | |
175 e1 : {y : Ordinal {n}} → def x y → def od∅ y | |
176 e1 {y} y<x = e0 ( o<-subst ( c<→o< {n} {x} y<x ) refl {!!} ) | |
177 e2 : {y : Ordinal {n}} → def od∅ y → def x y | |
178 e2 {y} (lift ()) | |
179 | |
180 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x | |
152 ∅9 x not = ∅5 ( od→ord x) lemma where | 181 ∅9 x not = ∅5 ( od→ord x) lemma where |
153 lemma : ¬ od→ord x ≡ o∅ | 182 lemma : ¬ od→ord x ≡ o∅ |
154 lemma eq = not ( ∅7 x eq ) | 183 lemma eq = not ( ∅7 x eq ) |
155 | 184 |
156 OD→ZF : {n : Level} → ZF {suc n} {suc n} | 185 OD→ZF : {n : Level} → ZF {suc n} {n} |
157 OD→ZF {n} = record { | 186 OD→ZF {n} = record { |
158 ZFSet = OD {n} | 187 ZFSet = OD {n} |
159 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x ) | 188 ; _∋_ = _∋_ |
160 ; _≈_ = _≡_ | 189 ; _≈_ = _==_ |
161 ; ∅ = od∅ | 190 ; ∅ = od∅ |
162 ; _,_ = _,_ | 191 ; _,_ = _,_ |
163 ; Union = Union | 192 ; Union = Union |
164 ; Power = Power | 193 ; Power = Power |
165 ; Select = Select | 194 ; Select = Select |
167 ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } } | 196 ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } } |
168 ; isZF = isZF | 197 ; isZF = isZF |
169 } where | 198 } where |
170 Replace : OD {n} → (OD {n} → OD {n} ) → OD {n} | 199 Replace : OD {n} → (OD {n} → OD {n} ) → OD {n} |
171 Replace X ψ = sup-od ψ | 200 Replace X ψ = sup-od ψ |
172 Select : OD {n} → (OD {n} → Set (suc n) ) → OD {n} | 201 Select : OD {n} → (OD {n} → Set n ) → OD {n} |
173 Select X ψ = record { def = λ x → select ( ord→od x ) } where | 202 Select X ψ = record { def = λ x → select ( ord→od x ) } where |
174 select : OD {n} → Set n | 203 select : OD {n} → Set n |
175 select x with ψ x | 204 select x = ψ x |
176 ... | t = Lift n ⊤ | |
177 _,_ : OD {n} → OD {n} → OD {n} | 205 _,_ : OD {n} → OD {n} → OD {n} |
178 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } | 206 x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } |
179 Union : OD {n} → OD {n} | 207 Union : OD {n} → OD {n} |
180 Union x = record { def = λ y → {z : Ordinal {n}} → def x z → def (ord→od z) y } | 208 Union x = record { def = λ y → {z : Ordinal {n}} → def x z → def (ord→od z) y } |
181 Power : OD {n} → OD {n} | 209 Power : OD {n} → OD {n} |
184 _∈_ : ( A B : ZFSet ) → Set n | 212 _∈_ : ( A B : ZFSet ) → Set n |
185 A ∈ B = B ∋ A | 213 A ∈ B = B ∋ A |
186 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set n | 214 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set n |
187 _⊆_ A B {x} = A ∋ x → B ∋ x | 215 _⊆_ A B {x} = A ∋ x → B ∋ x |
188 _∩_ : ( A B : ZFSet ) → ZFSet | 216 _∩_ : ( A B : ZFSet ) → ZFSet |
189 A ∩ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∧ (Lift (suc n) ( B ∋ x ) )) | 217 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) |
190 _∪_ : ( A B : ZFSet ) → ZFSet | 218 _∪_ : ( A B : ZFSet ) → ZFSet |
191 A ∪ B = Select (A , B) ( λ x → (Lift (suc n) ( A ∋ x )) ∨ (Lift (suc n) ( B ∋ x ) )) | 219 A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) |
192 infixr 200 _∈_ | 220 infixr 200 _∈_ |
193 infixr 230 _∩_ _∪_ | 221 infixr 230 _∩_ _∪_ |
194 infixr 220 _⊆_ | 222 infixr 220 _⊆_ |
195 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 } }) | 223 isZF : IsZF (OD {n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }) |
196 isZF = record { | 224 isZF = record { |
197 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } | 225 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } |
198 ; pair = pair | 226 ; pair = pair |
199 ; union→ = {!!} | 227 ; union→ = {!!} |
200 ; union← = {!!} | 228 ; union← = {!!} |
201 ; empty = empty | 229 ; empty = empty |
202 ; power→ = {!!} | 230 ; power→ = {!!} |
209 ; selection = {!!} | 237 ; selection = {!!} |
210 ; replacement = {!!} | 238 ; replacement = {!!} |
211 } where | 239 } where |
212 open _∧_ | 240 open _∧_ |
213 open Minimumo | 241 open Minimumo |
214 pair : (A B : OD {n} ) → Lift (suc n) ((A , B) ∋ A) ∧ Lift (suc n) ((A , B) ∋ B) | 242 pair : (A B : OD {n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) |
215 proj1 (pair A B ) = lift ( case1 refl ) | 243 proj1 (pair A B ) = case1 refl |
216 proj2 (pair A B ) = lift ( case2 refl ) | 244 proj2 (pair A B ) = case2 refl |
217 empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x) | 245 empty : (x : OD {n} ) → ¬ (od∅ ∋ x) |
218 empty x (lift (lift ())) | 246 empty x () |
219 union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y) | 247 union→ : (X x y : OD {n} ) → (X ∋ x) → (x ∋ y) → (Union X ∋ y) |
220 union→ X x y (lift X∋x) (lift x∋y) = lift {!!} where | 248 union→ X x y X∋x x∋y = {!!} where |
221 lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y | 249 lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y |
222 lemma {z} X∋z = {!!} | 250 lemma {z} X∋z = {!!} |
223 minord : (x : OD {n} ) → ¬ x ≡ od∅ → Minimumo (od→ord x) | 251 minord : (x : OD {n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x) |
224 minord x not = ominimal (od→ord x) (∅9 x not) | 252 minord x not = ominimal (od→ord x) (∅9 x not) |
225 minimul : (x : OD {n} ) → ¬ x ≡ od∅ → OD {n} | 253 minimul : (x : OD {n} ) → ¬ (x == od∅ )→ OD {n} |
226 minimul x not = ord→od ( mino (minord x not)) | 254 minimul x not = ord→od ( mino (minord x not)) |
227 minimul<x : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ minimul x not | 255 minimul<x : (x : OD {n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not |
228 minimul<x x not = lemma0 (min<x (minord x not)) where | 256 minimul<x x not = lemma0 (min<x (minord x not)) where |
229 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) | 257 lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) |
230 lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl | 258 lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl |
231 regularity : (x : OD) → (not : ¬ x ≡ od∅ ) → | 259 regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ |
232 Lift (suc n) (x ∋ minimul x not ) ∧ | 260 (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) |
233 (Select x (λ x₁ → Lift (suc n) ( minimul x not ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅) | 261 -- regularity : (x : OD) → (not : ¬ x == od∅ ) → |
234 proj1 ( regularity x non ) = lift ( minimul<x x non ) | 262 -- ((x ∋ minimul x not ) ∧ {!!} ) -- (Select x (λ x₁ → (( minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅))) |
235 proj2 ( regularity x non ) = cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) ) where | 263 proj1 ( regularity x non ) = minimul<x x non |
236 lemma : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z | 264 proj2 ( regularity x non ) = {!!} where -- cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) ) where |
237 lemma z with (minimul x non ∋ (ord→od z)) | x ∋ (ord→od z) | 265 not-min : ( z : Ordinal {n} ) → ¬ ( def (Select x (λ y → (minimul x non ∋ y) ∧ (x ∋ y))) z ) |
238 ... | s | t = {!!} | 266 not-min z = {!!} |
239 lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → Lift (suc n) (minimul x non ∋ y) ∧ Lift (suc n) (x ∋ y))) z ≡ Lift n ⊥ | 267 lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → (minimul x non ∋ y) ∧ (x ∋ y))) z ≡ Lift n ⊥ |
240 lemma0 = {!!} | 268 lemma0 z = {!!} |
241 | 269 |