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

comparison src/zorn1.agda @ 931:307ad8807963

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 Mon, 24 Oct 2022 04:30:41 +0900
parents 0e0608b1953b
children b1899e33e2c7
comparison
equal deleted inserted replaced
930:0e0608b1953b 931:307ad8807963
651 usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 651 usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y)
652 → ( supf : Ordinal → Ordinal ) 652 → ( supf : Ordinal → Ordinal )
653 → SUP A (UnionZF f mf ay supf ) 653 → SUP A (UnionZF f mf ay supf )
654 usp0 f mf ay supf = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf ) 654 usp0 f mf ay supf = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf )
655 655
656 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) 656 msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
657 → (zc : ZChain A f mf ay x ) 657 → (zc : ZChain A f mf ay x )
658 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) 658 → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x)
659 sp0 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where 659 msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
660 ztotal : IsTotalOrderSet (ZChain.chain zc) 660 ztotal : IsTotalOrderSet (ZChain.chain zc)
661 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 661 ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
662 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) 662 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
663 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) 663 uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb))
664
665 sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)
666 → (zc : ZChain A f mf ay x )
667 → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
668 sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc )
664 669
665 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) 670 fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) )
666 → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A) 671 → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A)
667 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) 672 → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc ))
668 fixpoint f mf zc ss<sa = ? 673 fixpoint f mf zc ss<sa = ?
678 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) 683 z04 nmx zc = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 ))))
679 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) 684 (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
680 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄ 685 (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄
681 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x 686 (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x
682 supf = ZChain.supf zc 687 supf = ZChain.supf zc
688 msp1 : MinSUP A (ZChain.chain zc)
689 msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
683 sp1 : SUP A (ZChain.chain zc) 690 sp1 : SUP A (ZChain.chain zc)
684 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 691 sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc
685 c = & (SUP.sup sp1) 692 c : Ordinal
686 z20 : c << cf nmx c 693 c = & ( SUP.sup sp1 )
687 z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) ) 694 mc = MinSUP.sup msp1
688 asc : odef A (supf c) 695 z20 : mc << cf nmx mc
696 z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) )
697 asc : odef A (supf mc)
689 asc = ZChain.asupf zc 698 asc = ZChain.asupf zc
690 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) 699 spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )
691 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc 700 spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc
692 d = MinSUP.sup spd 701 d = MinSUP.sup spd
693 d<A : d o< & A 702 d<A : d o< & A
722 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y ) 731 -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y )
723 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d 732 -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d
724 -- z25 (fsuc x lt) = ? -- cf (sup c) 733 -- z25 (fsuc x lt) = ? -- cf (sup c)
725 sd=d : supf d ≡ d 734 sd=d : supf d ≡ d
726 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ 735 sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫
727 sc<sd : supf c << supf d 736 sc<<sd : supf mc << supf d
728 sc<sd = ? 737 sc<<sd = ?
729 -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? ) 738 -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
730 -- sco<d : supf c o< supf d 739 sc<sd : supf mc o< supf d
731 -- sco<d with osuc-≡< ( ZChain.supf-<= zc (case2 sc<sd ) ) 740 sc<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) )
732 -- ... | case1 eq = ⊥-elim ( <-irr eq sc<sd ) 741 -- ... | case1 eq = ⊥-elim ( <-irr (case1 (subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq) )) sc<<sd )
733 -- ... | case2 lt = lt 742 ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) eq)) sc<<sd )
743 ... | case2 lt = lt
744
745 sms<sa : supf mc o< supf (& A)
746 sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) ))
747 ... | case2 lt = lt
748 ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ sc<sd ( ZChain.supf-mono zc (o<→≤ d<A ))))
734 749
735 ss<sa : supf c o< supf (& A) 750 ss<sa : supf c o< supf (& A)
736 ss<sa = ? -- with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ SUP.as sp0 , lift true ⟫) )) 751 ss<sa = ?
737 -- ... | case2 lt = lt 752
738 -- ... | case1 eq = ? -- where
739 zorn00 : Maximal A 753 zorn00 : Maximal A
740 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM 754 zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM
741 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where 755 ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where
742 -- yes we have the maximal 756 -- yes we have the maximal
743 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) 757 zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) )