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 ; _∋_ = _∋_ |