Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 298:3795ffb127d0
... should we use HOD?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 23 Jun 2020 11:14:30 +0900 |
parents | be6670af87fa |
children | 171f23379e2e |
comparison
equal
deleted
inserted
replaced
297:be6670af87fa | 298:3795ffb127d0 |
---|---|
71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) | 71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) |
72 field | 72 field |
73 maxod : Ordinal | 73 maxod : Ordinal |
74 od→ord : OD → Ordinal | 74 od→ord : OD → Ordinal |
75 ord→od : (x : Ordinal ) → x o< maxod → OD | 75 ord→od : (x : Ordinal ) → x o< maxod → OD |
76 -- ZFSet has bounded solution of OD | |
76 o<max : {x : OD } → od→ord x o< maxod | 77 o<max : {x : OD } → od→ord x o< maxod |
78 def<maxod : {x y : Ordinal} → (lt : x o< maxod) → def (ord→od x lt ) y → y o< maxod | |
77 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y | 79 c<→o< : {x y : OD } → def y ( od→ord x ) → od→ord x o< od→ord y |
78 oiso : {x : OD } → ord→od ( od→ord x ) o<max ≡ x | 80 oiso : {x : OD } → ord→od ( od→ord x ) o<max ≡ x |
79 diso : {x : Ordinal } → (lt : x o< maxod) → od→ord ( ord→od x lt ) ≡ x | 81 diso : {x : Ordinal } → (lt : x o< maxod) → od→ord ( ord→od x lt ) ≡ x |
80 ==→o≡ : { x y : OD } → (x == y) → x ≡ y | 82 ==→o≡ : { x y : OD } → (x == y) → x ≡ y |
81 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) | 83 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) |
105 | 107 |
106 od∅ : OD | 108 od∅ : OD |
107 od∅ = Ord o∅ | 109 od∅ = Ord o∅ |
108 | 110 |
109 | 111 |
112 -- = subst (λ k → k o< maxod ) (diso {!!}) ( ordtrans ( c<→o< lt ) o<max ) | |
110 -- o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y {!!} ) x ) → {x : OD } → x ≡ Ord (od→ord x) | 113 -- o<→c<→OD=Ord : ( {x y : Ordinal } → x o< y → def (ord→od y {!!} ) x ) → {x : OD } → x ≡ Ord (od→ord x) |
111 -- o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where | 114 -- o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where |
112 -- lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y | 115 -- lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y |
113 -- lemma1 {y} lt = subst ( λ k → k o< od→ord x ) (diso {!!}) (c<→o< {ord→od y {!!} } {x} (subst (λ k → def x k ) (sym (diso {!!})) lt)) | 116 -- lemma1 {y} lt = subst ( λ k → k o< od→ord x ) (diso {!!}) (c<→o< {ord→od y {!!} } {x} (subst (λ k → def x k ) (sym (diso {!!})) lt)) |
114 -- lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y | 117 -- lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y |
140 | 143 |
141 -- def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X | 144 -- def→o< : {X : OD } → {x : Ordinal } → def X x → x o< od→ord X |
142 -- def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym (diso lemma)))) (diso lemma) (diso o<max) where | 145 -- def→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( def-subst {X} {x} lt (sym oiso) (sym (diso lemma)))) (diso lemma) (diso o<max) where |
143 -- lemma : x o< maxod | 146 -- lemma : x o< maxod |
144 -- lemma = subst (λ k → k o< maxod ) (diso {!!} ) (otrans o<max ( c<→o< lt )) | 147 -- lemma = subst (λ k → k o< maxod ) (diso {!!} ) (otrans o<max ( c<→o< lt )) |
145 | |
146 | |
147 -- avoiding lv != Zero error | |
148 orefl : { x : OD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y | |
149 orefl refl = refl | |
150 | 148 |
151 ==-iso : { x y : OD } → ord→od (od→ord x) o<max == ord→od (od→ord y) o<max → x == y | 149 ==-iso : { x y : OD } → ord→od (od→ord x) o<max == ord→od (od→ord y) o<max → x == y |
152 ==-iso {x} {y} eq = record { | 150 ==-iso {x} {y} eq = record { |
153 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ; | 151 eq→ = λ d → lemma ( eq→ eq (def-subst d (sym oiso) refl )) ; |
154 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) } | 152 eq← = λ d → lemma ( eq← eq (def-subst d (sym oiso) refl )) } |
157 lemma {x} {z} d = def-subst d oiso refl | 155 lemma {x} {z} d = def-subst d oiso refl |
158 | 156 |
159 =-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) o<max == y) | 157 =-iso : {x y : OD } → (x == y) ≡ (ord→od (od→ord x) o<max == y) |
160 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) | 158 =-iso {_} {y} = cong ( λ k → k == y ) (sym oiso) |
161 | 159 |
160 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl) | |
161 -- | |
162 <-irr : {x y z : Ordinal } → x ≡ y → (x o< z) ≡ (y o< z) | 162 <-irr : {x y z : Ordinal } → x ≡ y → (x o< z) ≡ (y o< z) |
163 <-irr refl = refl | 163 <-irr refl = refl |
164 | 164 |
165 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y | 165 ord→== : { x y : OD } → od→ord x ≡ od→ord y → x == y |
166 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq) o<max o<max ) where | 166 ord→== {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) eq o<max o<max ) where |
167 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (x<m : ox o< maxod) (y<m : oy o< maxod) → (ord→od ox x<m ) == (ord→od oy y<m ) | 167 lemma : ( ox oy : Ordinal ) → ox ≡ oy → (x<m : ox o< maxod) (y<m : oy o< maxod) → (ord→od ox x<m ) == (ord→od oy y<m ) |
168 lemma ox ox refl x<m y<m = subst (λ k → ord→od ox x<m == ord→od ox k) {!!} ==-refl | 168 lemma ox ox refl x<m y<m = subst (λ k → ord→od ox x<m == ord→od ox k) {!!} ==-refl |
169 | 169 |
170 o≡→== : { x y : Ordinal } → x ≡ y → ord→od x {!!} == ord→od y {!!} | 170 o≡→== : { x y : Ordinal } → x ≡ y → (lx : x o< maxod ) → (ly : y o< maxod ) → ord→od x lx == ord→od y ly |
171 o≡→== {x} {.x} refl = ==-refl | 171 o≡→== {x} {.x} refl _ _ = {!!} -- ==-refl |
172 | 172 |
173 o∅≡od∅ : ord→od (o∅ ) {!!} ≡ od∅ | 173 o∅<maxod : o∅ o< maxod |
174 o∅<maxod with IsOrdinals.OTri (Ordinals.isOrdinal O) o∅ maxod | |
175 o∅<maxod | tri< a ¬b ¬c = a | |
176 o∅<maxod | tri≈ ¬a b ¬c = ⊥-elim (¬x<0 (subst (λ k → (od→ord record { def = λ x → One }) o< k ) (sym b) o<max )) | |
177 o∅<maxod | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) | |
178 | |
179 o∅≡od∅ : ord→od o∅ o∅<maxod ≡ od∅ | |
174 o∅≡od∅ = ==→o≡ lemma where | 180 o∅≡od∅ = ==→o≡ lemma where |
175 lemma0 : {x : Ordinal} → def (ord→od o∅ {!!} ) x → def od∅ x | 181 lemma0 : {x : Ordinal} → x o< maxod → def (ord→od o∅ o∅<maxod) x → def od∅ x |
176 lemma0 {x} lt = o<-subst (c<→o< {ord→od x {!!} } {ord→od o∅ {!!} } (def-subst {ord→od o∅ {!!} } {x} lt refl (sym (diso {!!} ))) ) (diso {!!}) (diso {!!}) | 182 lemma0 {x} x<m lt = o<-subst (c<→o< {ord→od x x<m } {ord→od o∅ o∅<maxod} |
177 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅ {!!} ) x | 183 (def-subst {ord→od o∅ o∅<maxod} {x} lt refl (sym (diso x<m ))) ) (diso x<m) (diso o∅<maxod) |
184 lemma1 : {x : Ordinal} → def od∅ x → def (ord→od o∅ o∅<maxod ) x | |
178 lemma1 {x} lt = ⊥-elim (¬x<0 lt) | 185 lemma1 {x} lt = ⊥-elim (¬x<0 lt) |
179 lemma : ord→od o∅ {!!} == od∅ | 186 lemma : ord→od o∅ o∅<maxod == od∅ |
180 lemma = record { eq→ = lemma0 ; eq← = lemma1 } | 187 lemma = record { eq→ = λ {x} lt → lemma0 (def<maxod o∅<maxod lt ) lt ; eq← = lemma1 } |
181 | 188 |
182 ord-od∅ : od→ord (od∅ ) ≡ o∅ | 189 ord-od∅ : od→ord (od∅ ) ≡ o∅ |
183 ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) (diso {!!}) (cong ( λ k → od→ord k ) o∅≡od∅ ) ) | 190 ord-od∅ = sym ( subst (λ k → k ≡ od→ord (od∅ ) ) (diso o∅<maxod) (cong ( λ k → od→ord k ) o∅≡od∅ ) ) |
184 | 191 |
185 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ | 192 ∅0 : record { def = λ x → Lift n ⊥ } == od∅ |
186 eq→ ∅0 {w} (lift ()) | 193 eq→ ∅0 {w} (lift ()) |
187 eq← ∅0 {w} lt = lift (¬x<0 lt) | 194 eq← ∅0 {w} lt = lift (¬x<0 lt) |
188 | 195 |
206 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) | 213 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y)) |
207 | 214 |
208 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | 215 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
209 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) | 216 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) |
210 | 217 |
218 | |
211 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD | 219 in-codomain : (X : OD ) → ( ψ : OD → OD ) → OD |
212 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧ ( x ≡ od→ord (ψ (ord→od y {!!} ))))) } | 220 in-codomain X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (lt : def X y ) → (lt : y o< maxod) → ( x ≡ od→ord (ψ (ord→od y lt ))))) } where |
213 | 221 |
214 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) | 222 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) |
215 | 223 |
216 ZFSubset : (A x : OD ) → OD | 224 ZFSubset : (A x : OD ) → OD |
217 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set | 225 ZFSubset A x = record { def = λ y → def A y ∧ def x y } -- roughly x = A → Set |
310 -- ; choice-func = choice-func | 318 -- ; choice-func = choice-func |
311 -- ; choice = choice | 319 -- ; choice = choice |
312 } where | 320 } where |
313 | 321 |
314 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) | 322 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y ) |
315 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x )) | 323 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x {!!} {!!} )) |
316 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y )) | 324 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y {!!} {!!} )) |
317 | 325 |
318 pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t | 326 pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t |
319 pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) | 327 pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x)) |
320 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) | 328 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y)) |
321 | 329 |
348 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } | 356 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) oiso } |
349 } | 357 } |
350 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x | 358 replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x |
351 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where | 359 replacement← {ψ} X x lt = record { proj1 = sup-c< ψ {x} ; proj2 = lemma } where |
352 lemma : def (in-codomain X ψ) (od→ord (ψ x)) | 360 lemma : def (in-codomain X ψ) (od→ord (ψ x)) |
353 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) | 361 lemma not = ⊥-elim ( not ( od→ord x ) {!!} ) -- (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} )) |
354 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) | 362 replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y)) |
355 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where | 363 replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where |
356 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} )))) | 364 lemma2 : ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y {!!} )))) |
357 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))) | 365 → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} ))) |
358 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where | 366 lemma2 not not2 = not ( λ y d → not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where |
359 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) | 367 lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od y {!!} ))) → (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) |
360 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq ) | 368 lemma3 {y} eq = subst (λ k → ord→od (od→ord x) {!!} == k ) oiso (o≡→== eq {!!} {!!} ) |
361 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) ) | 369 lemma : ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) {!!} == ψ (ord→od y {!!} )) ) |
362 lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso ( proj2 not2 )) | 370 lemma not y not2 = not (ord→od y {!!} ) (subst (λ k → k == ψ (ord→od y {!!} )) oiso ( proj2 not2 )) |
363 | 371 |
364 --- | 372 --- |
365 --- Power Set | 373 --- Power Set |
431 ∎ | 439 ∎ |
432 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) | 440 lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ x)) |
433 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) | 441 lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ x))) |
434 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) | 442 lemma4 (sup-o< {λ x → od→ord (A ∩ x)} ) |
435 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) | 443 lemma2 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) |
436 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where | 444 lemma2 not = ⊥-elim ( not (od→ord t) {!!}) where -- (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where |
437 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t) {!!} ) | 445 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t) {!!} ) |
438 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) | 446 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A ))) |
439 | 447 |
440 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) | 448 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) |
441 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where | 449 ord⊆power a = record { incl = λ {x} lt → power← (Ord a) x (lemma lt) } where |