Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/OD.agda @ 1109:f46a16cebbab
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 31 Dec 2022 17:56:01 +0900 |
parents | 40345abc0949 |
children | 607a79aef297 |
comparison
equal
deleted
inserted
replaced
1108:720aff4a7fa4 | 1109:f46a16cebbab |
---|---|
293 ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where | 293 ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where |
294 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) | 294 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) |
295 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) | 295 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) |
296 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) | 296 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) |
297 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy | 297 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy |
298 | |
299 ε-induction0 : { ψ : HOD → Set n} | |
300 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) | |
301 → (x : HOD ) → ψ x | |
302 ε-induction0 {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc ) where | |
303 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox) | |
304 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso ))) | |
305 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy) | |
306 ε-induction-ord ox {oy} lt = inOrdinal.TransFinite0 O {λ oy → ψ (* oy)} induction oy | |
298 | 307 |
299 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup | 308 -- Open supreme upper bound leads a contradition, so we use domain restriction on sup |
300 ¬open-sup : ( sup-o : (Ordinal → Ordinal ) → Ordinal) → ((ψ : Ordinal → Ordinal ) → (x : Ordinal) → ψ x o< sup-o ψ ) → ⊥ | 309 ¬open-sup : ( sup-o : (Ordinal → Ordinal ) → Ordinal) → ((ψ : Ordinal → Ordinal ) → (x : Ordinal) → ψ x o< sup-o ψ ) → ⊥ |
301 ¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where | 310 ¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where |
302 next-ord : Ordinal → Ordinal | 311 next-ord : Ordinal → Ordinal |