Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 330:0faa7120e4b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Jul 2020 15:49:00 +0900
parents 72f3e3b44c27
children daafa2213dd2
comparison
equal deleted inserted replaced
329:5544f4921a44 330:0faa7120e4b5
257 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where 257 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where
258 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 258 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
259 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 259 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
260 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 260 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
261 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy 261 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
262
263 ε-induction1 : { ψ : HOD → Set (suc n)}
264 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
265 → (x : HOD ) → ψ x
266 ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where
267 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
268 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
269 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
270 ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
262 271
263 HOD→ZF : ZF 272 HOD→ZF : ZF
264 HOD→ZF = record { 273 HOD→ZF = record {
265 ZFSet = HOD 274 ZFSet = HOD
266 ; _∋_ = _∋_ 275 ; _∋_ = _∋_