Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/zorn.agda @ 1060:a09f5e728f92
IChain?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 11 Dec 2022 08:48:42 +0900 |
parents | bd2a258f309c |
children | fc37082d2a8a |
comparison
equal
deleted
inserted
replaced
1059:bd2a258f309c | 1060:a09f5e728f92 |
---|---|
274 data UChain { A : HOD } { f : Ordinal → Ordinal } {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) | 274 data UChain { A : HOD } { f : Ordinal → Ordinal } {supf : Ordinal → Ordinal} {y : Ordinal } (ay : odef A y ) |
275 (x : Ordinal) : (z : Ordinal) → Set n where | 275 (x : Ordinal) : (z : Ordinal) → Set n where |
276 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z | 276 ch-init : {z : Ordinal } (fc : FClosure A f y z) → UChain ay x z |
277 ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z | 277 ch-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u ≡ u) ( fc : FClosure A f (supf u) z ) → UChain ay x z |
278 | 278 |
279 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD | 279 UnionCF : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( supf : Ordinal → Ordinal ) ( x : Ordinal ) → HOD |
280 UnionCF A f ay supf x | 280 UnionCF A f ay supf x |
281 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; | 281 = record { od = record { def = λ z → odef A z ∧ UChain {A} {f} {supf} ay x z } ; |
282 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } | 282 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } |
283 | 283 |
284 -- Union of all UChain under limit ordinal x | |
285 | |
286 data IChain { A : HOD } { f : Ordinal → Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) {y : Ordinal } (ay : odef A y ) | |
287 (x : Ordinal) : (z : Ordinal) → Set n where | |
288 ic-init : {z : Ordinal } (fc : FClosure A f y z) → IChain supf ay x z | |
289 ic-is-sup : (u : Ordinal) {z : Ordinal } (u<x : u o< x) (supu=u : supf u<x u ≡ u) ( fc : FClosure A f (supf u<x u) z ) → IChain supf ay x z | |
290 | |
291 UnionIC : ( A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) (supfz : {z : Ordinal } → z o< x → Ordinal) ( x : Ordinal ) → HOD | |
292 UnionIC A f ay supf x | |
293 = record { od = record { def = λ z → odef A z ∧ IChain {A} {f} supf ay x z } ; | |
294 odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } | |
284 | 295 |
285 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) | 296 supf-inject0 : {x y : Ordinal } {supf : Ordinal → Ordinal } → (supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y ) |
286 → supf x o< supf y → x o< y | 297 → supf x o< supf y → x o< y |
287 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y | 298 supf-inject0 {x} {y} {supf} supf-mono sx<sy with trio< x y |
288 ... | tri< a ¬b ¬c = a | 299 ... | tri< a ¬b ¬c = a |
504 record Maximal ( A : HOD ) : Set (Level.suc n) where | 515 record Maximal ( A : HOD ) : Set (Level.suc n) where |
505 field | 516 field |
506 maximal : HOD | 517 maximal : HOD |
507 as : A ∋ maximal | 518 as : A ∋ maximal |
508 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative | 519 ¬maximal<x : {x : HOD} → A ∋ x → ¬ maximal < x -- A is Partial, use negative |
509 | |
510 record IChain (A : HOD) ( f : Ordinal → Ordinal ) {x : Ordinal } (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where | |
511 field | |
512 i : Ordinal | |
513 i<x : i o< x | |
514 fc : FClosure A f (supfz i<x) z | |
515 | 520 |
516 -- | 521 -- |
517 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup | 522 -- supf in TransFinite indution may differ each other, but it is the same because of the minimul sup |
518 -- | 523 -- |
519 supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) | 524 supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) |
1238 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where | 1243 ; zo≤sz = ? ; supfmax = λ _ → refl ; is-minsup = ? ; cfcs = ? } where |
1239 mf : ≤-monotonic-f A f | 1244 mf : ≤-monotonic-f A f |
1240 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where | 1245 mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where |
1241 mf00 : * x < * (f x) | 1246 mf00 : * x < * (f x) |
1242 mf00 = proj1 ( mf< x ax ) | 1247 mf00 = proj1 ( mf< x ax ) |
1243 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = ? ; supf-mono = supf-mono ; order = ? | 1248 ... | tri> ¬a ¬b 0<x = record { supf = supf1 ; asupf = asupf ; supf-mono = supf-mono ; order = ? |
1244 ; zo≤sz = λ _ → ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where | 1249 ; zo≤sz = ? ; supfmax = ? ; is-minsup = ? ; cfcs = cfcs } where |
1245 | 1250 |
1246 -- mf : ≤-monotonic-f A f | 1251 -- mf : ≤-monotonic-f A f |
1247 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust | 1252 -- mf x ax = ? -- ⟪ case2 ( proj1 (mf< x ax)) , proj2 (mf< x ax ) ⟫ will result memory exhaust |
1248 | 1253 |
1249 mf : ≤-monotonic-f A f | 1254 mf : ≤-monotonic-f A f |