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

comparison src/zorn.agda @ 866:8a49ab1dcbd0

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, 11 Sep 2022 19:58:49 +0900
parents b095c84310df
children 166bee3ddf4c
comparison
equal deleted inserted replaced
865:b095c84310df 866:8a49ab1dcbd0
349 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy ) 349 ... | tri≈ ¬a refl ¬c = ⊥-elim ( o<¬≡ (cong supf refl) sx<sy )
350 ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) ) 350 ... | tri> ¬a ¬b y<x with osuc-≡< (supf-mono (o<→≤ y<x) )
351 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy ) 351 ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
352 ... | case2 lt = ⊥-elim ( o<> sx<sy lt ) 352 ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
353 353
354 record Zsupf ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 354 zsupf0 : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y)
355 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition
356 → { z : Ordinal } → (odef A z) → SUP A (UnionCF A f mf ay (λ _ → z) z)
357 zsupf0 A f mf ay supP {z} az = supP chain (λ lt → proj1 lt ) f-total where
358 chain = UnionCF A f mf ay (λ _ → z) z
359 f-total : IsTotalOrderSet chain
360 f-total {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
361 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
362 uz01 = chain-total A f mf ay (λ _ → z) ( (proj2 ca)) ( (proj2 cb))
363
364 record ZSupf ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
355 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 365 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
356 field 366 field
357 s : Ordinal 367 supf : Ordinal → Ordinal
358 s=z : odef A z → s ≡ z 368 sup : (x : Ordinal ) → SUP A (UnionCF A f mf ay (λ _ → z) x)
359 as : odef A s 369 supf-is-sup : {x : Ordinal } → supf x ≡ & (SUP.sup (sup x) )
360 sup : SUP A (UnionCF A f mf ay (λ _ → s) z) 370 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
371
372
373 zsupf : (A : HOD) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)
374 → ( ( B : HOD) → (B⊆A : B ⊆' A) → IsTotalOrderSet B → SUP A B ) -- SUP condition
375 → (x : Ordinal) → ZSupf A f mf ay x
376 zsupf A f mf {y} ay supP x = TransFinite { λ x → ZSupf A f mf ay x } zc1 x where
377
378 zc1 : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → ZSupf A f mf ay y₁) → ZSupf A f mf ay x
379 zc1 x prev with Oprev-p x
380 ... | yes op = record { supf = ? ; sup = ? ; spuf-is-sup = ? ; supf-mono = ? } where
381 px = Oprev.oprev op
382 zc-b<x : {b : Ordinal } → b o< x → b o< osuc px
383 zc-b<x {b} lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt
384 supf : Ordinal → Ordinal
385 supf z with trio< z px
386 ... | tri< a ¬b ¬c = ZSupf.spuf (prev (ordtrans a (pxo<x op))) z
387 ... | tri≈ ¬a b ¬c = ZSupf.spuf (prev (subst (λ k → k o< x ) b (pxo<x op))) z
388 ... | tri> ¬a ¬b px<x with ODC.∋-p O A (* x)
389 ... | no noax = ZSupf.spuf (prev o≤-refl ) px
390 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )
391 ... | case1 pr = ZSupf.spuf (prev o≤-refl ) px
392 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
393 ... | case2 ¬x=sup = ZSupf.spuf (prev o≤-refl ) px
394 ... | case1 is-sup = ?
395
396 ... | no lim = ? where
397
398 -- Range of supf is total order set, so it has SUP
399 supfmax : Ordinal
400 supfmax = ?
401
402 supfx : Ordinal
403 supfx with ODC.∋-p O A (* x)
404 ... | no noax = supfmax
405 ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc ) z f )
406 ... | case1 pr = supfmax
407 ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc ) ax )
408 ... | case2 ¬x=sup = supfmax
409 ... | case1 is-sup = ?
410
411 supf : Ordinal → Ordinal
412 supf z with trio< z x
413 ... | tri< a ¬b ¬c = ZSupf.spuf a z
414 ... | tri≈ ¬a b ¬c = supfx
415 ... | tri> ¬a ¬b px<x = supfx
416
361 417
362 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 418 record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
363 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where 419 {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
364 field 420 field
365 supf : Ordinal → Ordinal 421 supf : Ordinal → Ordinal