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

comparison src/zorn.agda @ 928:330303f0c688

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 Sat, 22 Oct 2022 11:15:17 +0900
parents 0f2a85826cc7
children a6d97e6e5309
comparison
equal deleted inserted replaced
927:0f2a85826cc7 928:330303f0c688
694 utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 694 utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
695 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 695 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
696 uz01 = fcn-cmp y f mf ca cb 696 uz01 = fcn-cmp y f mf ca cb
697 697
698 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 698 ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
699 → SUP A (uchain f mf ay) 699 → MinSUP A (uchain f mf ay)
700 ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay) 700 ysup f mf {y} ay = minsupP (uchain f mf ay) (λ lt → A∋fc y f mf lt) (utotal f mf ay)
701 701
702 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B 702 SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
703 SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) } 703 SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt) }
704 704
705 record xSUP (B : HOD) (x : Ordinal) : Set n where 705 record xSUP (B : HOD) (x : Ordinal) : Set n where
1195 ... | no lim = zc5 where 1195 ... | no lim = zc5 where
1196 1196
1197 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z 1197 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
1198 pzc z z<x = prev z z<x 1198 pzc z z<x = prev z z<x
1199 1199
1200 ysp = & (SUP.sup (ysup f mf ay)) 1200 ysp = MinSUP.sup (ysup f mf ay)
1201 1201
1202 supf0 : Ordinal → Ordinal 1202 supf0 : Ordinal → Ordinal
1203 supf0 z with trio< z x 1203 supf0 z with trio< z x
1204 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z 1204 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
1205 ... | tri≈ ¬a b ¬c = ysp 1205 ... | tri≈ ¬a b ¬c = ysp
1412 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x 1412 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
1413 supf = ZChain.supf zc 1413 supf = ZChain.supf zc
1414 sp1 : SUP A (ZChain.chain zc) 1414 sp1 : SUP A (ZChain.chain zc)
1415 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 1415 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
1416 c = & (SUP.sup sp1) 1416 c = & (SUP.sup sp1)
1417 d : Ordinal 1417 z20 : c << cf nmx c
1418 d = cf nmx (supf c ) 1418 z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) )
1419 z21 : d o< & A 1419 asc : odef A (supf c)
1420 z21 = ∈∧P→o< ⟪ proj2 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc)) , lift true ⟫ 1420 asc = ZChain.asupf zc
1421 z20 : supf c << d 1421 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )
1422 z20 = proj1 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc) ) 1422 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc
1423 d = MinSUP.sup spd
1424 d<A : d o< & A
1425 d<A = ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
1426 sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
1427 sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
1428 sd=d : supf d ≡ d
1429 sd=d = ?
1430 sc<d : supf c << d
1431 sc<d = ? where
1432 z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
1433 sco<d : supf c o< supf d
1434 sco<d = ?
1435
1423 ss<sa : supf c o< supf (& A) 1436 ss<sa : supf c o< supf (& A)
1424 ss<sa = ? 1437 ss<sa with osuc-≡< ( ZChain.supf-mono zc ? )
1438 ... | case2 lt = lt
1439 ... | case1 eq = ? -- where
1425 zorn00 : Maximal A 1440 zorn00 : Maximal A
1426 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 1441 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
1427 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where 1442 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where
1428 -- yes we have the maximal 1443 -- yes we have the maximal
1429 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) 1444 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )