Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 261:d9d178d1457c
ε-induction from TransFinite induction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 17 Sep 2019 09:29:27 +0900 |
| parents | 8b85949bde00 |
| children | 53744836020b |
comparison
equal
deleted
inserted
replaced
| 260:8b85949bde00 | 261:d9d178d1457c |
|---|---|
| 347 subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) | 347 subset-lemma : {A x y : OD } → ( x ∋ y → ZFSubset A x ∋ y ) ⇔ ( _⊆_ x A {y} ) |
| 348 subset-lemma {A} {x} {y} = record { | 348 subset-lemma {A} {x} {y} = record { |
| 349 proj1 = λ z lt → proj1 (z lt) | 349 proj1 = λ z lt → proj1 (z lt) |
| 350 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } | 350 ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt } |
| 351 } | 351 } |
| 352 | |
| 353 open import Data.Unit | |
| 354 | |
| 355 ε-induction : { ψ : OD → Set (suc n)} | |
| 356 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x ) | |
| 357 → (x : OD ) → ψ x | |
| 358 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where | |
| 359 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) | |
| 360 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) | |
| 361 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) | |
| 362 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy | |
| 352 | 363 |
| 353 OD→ZF : ZF | 364 OD→ZF : ZF |
| 354 OD→ZF = record { | 365 OD→ZF = record { |
| 355 ZFSet = OD | 366 ZFSet = OD |
| 356 ; _∋_ = _∋_ | 367 ; _∋_ = _∋_ |