Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 175:51189f7b9229
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 17:16:43 +0900 |
parents | ad7a6185b6d5 |
children | ecb329ba38ac |
comparison
equal
deleted
inserted
replaced
174:ad7a6185b6d5 | 175:51189f7b9229 |
---|---|
283 lemma z lt | case2 lz=ly with <-cmp lx ly | 283 lemma z lt | case2 lz=ly with <-cmp lx ly |
284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen | 284 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen |
285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) | 285 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- z(b) |
286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) | 286 ... | eq = subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c ))) |
287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) | 287 lemma z lt | case2 lz=ly | tri≈ ¬a refl ¬c with d<→lv lz=ly -- z(c) |
288 ... | eq = subst ( λ k → ψ k ) oiso (lemma6 {lx} {lv (od→ord (ord→od (record { lv = lx ; ord = oy })))} {lv (od→ord z)} | 288 ... | eq = lemma6 {lx} {ly} {lv (od→ord z)} {Φ lx} {oy} {ord (od→ord z)} {!!} ? ? where |
289 {oy} {_} (sym lemma1) (sym eq) (trans (sym lemma1) (sym eq)) lz=ly ) where | |
290 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z | 289 lemma5 : (ox : OrdinalD lx) → (lv (od→ord z) < lx) ∨ (ord (od→ord z) d< ox) → ψ z |
291 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) | 290 lemma5 ox lt = subst (λ k → ψ k ) oiso (ε-induction-ord lx ox lt ) |
292 lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } → | 291 lemma6 : { lx ly lz : Nat } { ox : OrdinalD {suc n} lx } { oy : OrdinalD {suc n} ly } { oz : OrdinalD {suc n} lz } → |
293 lx ≡ ly → ly ≡ lz → lx ≡ lz → oz d< oy → ψ (ord→od ( record { lv = lz ; ord = oz} )) | 292 lx ≡ ly → ly ≡ lz → oz d< oy → ψ z |
294 lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl refl _ = ? -- subst ( λ k → ψ k ) (sym oiso) ( lemma5 {!!} {!!} ) | 293 lemma6 {lx} {ly} {lz} {ox} {oy} {oz} refl refl _ = lemma5 {!!} (case2 {!!} ) |
295 | 294 |
296 | 295 |
297 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 296 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
298 OD→ZF {n} = record { | 297 OD→ZF {n} = record { |
299 ZFSet = OD {suc n} | 298 ZFSet = OD {suc n} |