Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 168:b25a4eca06a6
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 03:27:58 +0900 |
parents | 4724f7be00e3 |
children | acbcbd98d588 |
comparison
equal
deleted
inserted
replaced
167:4724f7be00e3 | 168:b25a4eca06a6 |
---|---|
465 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 465 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
466 choice-func X {x} not X∋x = minimul x not | 466 choice-func X {x} not X∋x = minimul x not |
467 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 467 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
468 choice X {A} X∋A not = x∋minimul A not | 468 choice X {A} X∋A not = x∋minimul A not |
469 | 469 |
470 -- another form of regularity | |
471 -- | |
470 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 472 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
471 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 473 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |
472 → (x : OD {suc n} ) → ψ x | 474 → (x : OD {suc n} ) → ψ x |
473 ε-induction {n} {m} {ψ} ind x with od→ord x | oiso {suc n} {x} | 475 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where |
474 ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = Φ 0 } | refl = ind (lemma o∅≡od∅ ) where | 476 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) |
475 lemma : { y : OD {suc n} } → x ≡ od∅ → x ∋ y → ψ y | 477 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ()) |
476 lemma {y} eq lt with empty y (o<-subst (c<→o< lt) refl diso ) | 478 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ()) |
477 lemma {y} eq lt | () | 479 ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = |
478 ε-induction {n} {m} {ψ} ind x | record { lv = Zero ; ord = OSuc 0 ox } | refl = {!!} | 480 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where |
479 ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = Φ (Suc lx) } | refl = {!!} | 481 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } |
480 ε-induction {n} {m} {ψ} ind x | record { lv = Suc lx ; ord = OSuc (Suc lx) ox } | refl = {!!} | 482 lemma y lt with osuc-≡< y<x |
481 | 483 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso |
482 -- subst (λ k → ψ k ) oiso (TransFinite {suc n} {suc (suc n) ⊔ m} {λ x → ({y : Ordinal } → y o< x → ψ y ) → ψ (ord→od x) } {!!} {!!} {!!} {!!}) | 484 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 |
485 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = OSuc ly oy }} (case1 (s≤s x)) = | |
486 ind {ord→od record { lv = ly ; ord = OSuc ly oy }} ( | |
487 λ {y} lt → subst ( λ k → ψ k ) oiso ( ε-induction-ord record { lv = lx ; ord = (Φ lx) } {od→ord y} {!!})) where | |
488 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = Φ ly }} (case1 (s≤s x)) = {!!} | |
489 |