Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 339:feb0fcc430a9
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 12 Jul 2020 19:55:37 +0900 |
parents | bca043423554 |
children | 639fbb6284d8 |
comparison
equal
deleted
inserted
replaced
338:bca043423554 | 339:feb0fcc430a9 |
---|---|
101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x | 101 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x |
102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y | 102 ==→o≡ : {x y : HOD } → (od x == od y) → x ≡ y |
103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal | 103 sup-o : (A : HOD) → ( ( x : Ordinal ) → def (od A) x → Ordinal ) → Ordinal |
104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ | 104 sup-o< : (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x → Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o< sup-o A ψ |
105 | 105 |
106 -- another form of infinite | |
107 -- pair-ord< : {x : Ordinal } → od→ord ( ord→od x , ord→od x ) o< next (od→ord x) | |
108 | |
109 postulate odAxiom : ODAxiom | 106 postulate odAxiom : ODAxiom |
110 open ODAxiom odAxiom | 107 open ODAxiom odAxiom |
108 | |
109 -- possible restriction | |
110 hod-ord< : {x : HOD } → Set n | |
111 hod-ord< {x} = od→ord x o< next (odmax x) | |
111 | 112 |
112 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD | 113 -- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD |
113 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ | 114 ¬OD-order : ( od→ord : OD → Ordinal ) → ( ord→od : Ordinal → OD ) → ( { x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥ |
114 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) | 115 ¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj ) |
115 | 116 |
219 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where | 220 x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x) (od→ord y) ; <odmax = lemma } where |
220 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) | 221 lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y) |
221 lemma {t} (case1 refl) = omax-x _ _ | 222 lemma {t} (case1 refl) = omax-x _ _ |
222 lemma {t} (case2 refl) = omax-y _ _ | 223 lemma {t} (case2 refl) = omax-y _ _ |
223 | 224 |
225 -- another form of infinite | |
226 pair-ord< : {x : Ordinal } → Set n | |
227 pair-ord< {x} = od→ord ( ord→od x , ord→od x ) o< next x | |
224 | 228 |
225 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | 229 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
226 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) | 230 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) |
227 | 231 |
228 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD | 232 in-codomain : (X : HOD ) → ( ψ : HOD → HOD ) → OD |
368 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax | 372 <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax |
369 | 373 |
370 infinite : HOD | 374 infinite : HOD |
371 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } | 375 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } |
372 | 376 |
373 -- infinite' : HOD | 377 infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD |
374 -- infinite' = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where | 378 infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma } where |
375 -- u : (y : Ordinal ) → HOD | 379 u : (y : Ordinal ) → HOD |
376 -- u y = Union (ord→od y , (ord→od y , ord→od y)) | 380 u y = Union (ord→od y , (ord→od y , ord→od y)) |
377 -- lemma : {y : Ordinal} → infinite-d y → y o< next o∅ | 381 lemma : {y : Ordinal} → infinite-d y → y o< next o∅ |
378 -- lemma {o∅} iφ = {!!} | 382 lemma {o∅} iφ = proj1 next-limit |
379 -- lemma (isuc {y} x) = {!!} where | 383 lemma (isuc {y} x) = lemma2 where |
380 -- lemma1 : od→ord (Union (ord→od y , (ord→od y , ord→od y))) o< od→ord (Union (u y , (u y , u y ))) | 384 lemma0 : y o< next o∅ |
381 -- lemma1 = {!!} | 385 lemma0 = lemma x |
386 lemma3 : odef (u y ) y | |
387 lemma3 = FExists _ (λ {z} t not → not (od→ord (ord→od y , ord→od y)) record { proj1 = case2 refl ; proj2 = lemma4 }) (λ not → not y (infinite-d y)) where | |
388 lemma4 : def (od (ord→od (od→ord (ord→od y , ord→od y)))) y | |
389 lemma4 = subst₂ ( λ j k → def (od j) k ) (sym oiso) diso (case1 refl) | |
390 lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y)))) | |
391 lemma1 = ho< | |
392 lemma2 : od→ord (u y) o< next o∅ | |
393 lemma2 = {!!} | |
382 | 394 |
383 | 395 |
384 _=h=_ : (x y : HOD) → Set n | 396 _=h=_ : (x y : HOD) → Set n |
385 x =h= y = od x == od y | 397 x =h= y = od x == od y |
386 | 398 |