Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 328:72f3e3b44c27
intoduce ωmax
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 05 Jul 2020 11:40:55 +0900 |
| parents | cde56f704eac |
| children | 0faa7120e4b5 |
comparison
equal
deleted
inserted
replaced
| 327:cde56f704eac | 328:72f3e3b44c27 |
|---|---|
| 317 data infinite-d : ( x : Ordinal ) → Set n where | 317 data infinite-d : ( x : Ordinal ) → Set n where |
| 318 iφ : infinite-d o∅ | 318 iφ : infinite-d o∅ |
| 319 isuc : {x : Ordinal } → infinite-d x → | 319 isuc : {x : Ordinal } → infinite-d x → |
| 320 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) | 320 infinite-d (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) )) |
| 321 | 321 |
| 322 -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair. | |
| 323 -- We simply assumes nfinite-d y has a maximum. | |
| 324 -- | |
| 325 -- This means that many of OD cannot be HODs because of the od→ord mapping divergence. | |
| 326 -- We should have some axioms to prevent this, but it may complicate thins. | |
| 327 -- | |
| 328 postulate | |
| 329 ωmax : Ordinal | |
| 330 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax | |
| 331 | |
| 322 infinite : HOD | 332 infinite : HOD |
| 323 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where | 333 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } |
| 324 u : HOD → HOD | |
| 325 u x = Union (x , (x , x)) | |
| 326 lemma1 : {x : HOD} → u x ⊆ Union (u x , (u x , u x)) | |
| 327 lemma1 {x} = record { incl = λ {y} lt → lemma2 y lt } where | |
| 328 lemma2 : (y : HOD) → u x ∋ y → ((z : Ordinal) → (z ≡ od→ord (u x)) ∨ (z ≡ od→ord (u x , u x)) ∧ def (od (ord→od z)) (od→ord y) → ⊥) → ⊥ | |
| 329 lemma2 y lt not = not (od→ord (u x)) record { proj1 = case1 refl ; proj2 = subst (λ k → def (od k) (od→ord y) ) (sym oiso) lt } | |
| 330 lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x)) )) | |
| 331 lemma3 {x} = od⊆→o≤ lemma1 | |
| 332 lemma6 : {x y : HOD} → y ≡ u x → HOD | |
| 333 lemma6 {x} _ = x | |
| 334 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ | |
| 335 lemma {y} = TransFinite {λ x → infinite-d x → x o< next o∅ } ind y where | |
| 336 ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅)) → | |
| 337 infinite-d x → x o< (next o∅) | |
| 338 ind o∅ prev iφ = proj1 next-limit | |
| 339 ind x prev (isuc lt) = lemma0 {_} {x} {!!} where | |
| 340 lemma0 : {x z : Ordinal} → x o< od→ord (Union (ord→od z , (ord→od z , ord→od z))) → od→ord (Union (ord→od x , (ord→od x , ord→od x))) o< next o∅ | |
| 341 lemma0 {x} with prev x {!!} | |
| 342 ... | t = {!!} | |
| 343 | 334 |
| 344 _=h=_ : (x y : HOD) → Set n | 335 _=h=_ : (x y : HOD) → Set n |
| 345 x =h= y = od x == od y | 336 x =h= y = od x == od y |
| 346 | 337 |
| 347 infixr 200 _∈_ | 338 infixr 200 _∈_ |