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

comparison src/zorn.agda @ 835:106492766e36

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 Tue, 23 Aug 2022 15:16:06 +0900
parents 6bf0899a6150
children d72bcf8552bb
comparison
equal deleted inserted replaced
834:6bf0899a6150 835:106492766e36
693 pcy : odef pchain y 693 pcy : odef pchain y
694 pcy = ⟪ ay , ch-init (init ay refl) ⟫ 694 pcy = ⟪ ay , ch-init (init ay refl) ⟫
695 695
696 supf0 = ZChain.supf zc 696 supf0 = ZChain.supf zc
697 697
698 sup1 : SUP A (UnionCF A f mf ay supf0 px)
699 sup1 = supP pchain pchain⊆A ptotal
700 sp1 = & (SUP.sup sup1 )
701 supf1 : Ordinal → Ordinal
702 supf1 z with trio< z px
703 ... | tri< a ¬b ¬c = ZChain.supf zc z
704 ... | tri≈ ¬a b ¬c = sp1
705 ... | tri> ¬a ¬b c = sp1
706
707 pchain1 : HOD
708 pchain1 = UnionCF A f mf ay supf1 x
709
710
698 -- if previous chain satisfies maximality, we caan reuse it 711 -- if previous chain satisfies maximality, we caan reuse it
699 -- 712 --
700 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x 713 -- supf0 px is sup of UnionCF px , supf0 x is sup of UnionCF x
701 714
702 no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x 715 no-extension : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain ? f → ZChain A f mf ay x
772 ... | no lim = zc5 where 785 ... | no lim = zc5 where
773 786
774 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z 787 pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
775 pzc z z<x = prev z z<x 788 pzc z z<x = prev z z<x
776 789
777 record Usupf : Set n where 790 ysp = & (SUP.sup (ysup f mf ay))
778 field 791
779 umax : Ordinal → Ordinal 792 initial-segment : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x) → a o< b → z o≤ a
780 umax<x : {z : Ordinal } → umax z o< x 793 → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z ≡ ZChain.(umax z)) (ob<x lim b<x )) z
781 supf : Ordinal → Ordinal
782 supf z = ZChain.supf (pzc (osuc (umax z)) (ob<x lim umax<x )) z
783 field
784 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
785
786 initial-segment : {a b z : Ordinal } → (a<x : a o< x ) → (b<x : b o< x )
787 → a o≤ b
788 → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) z o≤ ZChain.supf (pzc (osuc b) (ob<x lim b<x )) z
789 initial-segment = ? 794 initial-segment = ?
790 795
791 is01 : {a b : Ordinal } → (a<x : a o< x ) → (b<x : b o< x ) 796 initial-segment1 : {a b z : Ordinal } → (a<x : a o< x) ( b<x : b o< x) → a o< b →
792 → a o≤ b 797 → ZChain.supf (pzc (osuc a) (ob<x lim a<x )) x ≡ ZChain.(umax z)) (ob<x lim b<x )) x
793 UnionCF A f mf ay (ZChain.supf (pzc (osuc a) (ob<x lim a<x ))) x ⊆' 798 initial-segment1 = ?
794 UnionCF A f mf ay (ZChain.supf (pzc (osuc b) (ob<x lim b<x ))) x 799
795 is01 = ? 800 supf0 : Ordinal → Ordinal
801 supf0 z with trio< z x
802 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
803 ... | tri≈ ¬a b ¬c = {!!}
804 ... | tri> ¬a ¬b c = {!!}
805
806 pchain0 : HOD
807 pchain0 = UnionCF A f mf ay supf0 x
808
809 ptotal0 : IsTotalOrderSet pchain0
810 ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where
811 uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
812 uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb))
813
814 usup : SUP A pchain0
815 usup = supP pchain0 (λ lt → proj1 lt) ptotal0
816 spu = & (SUP.sup usup)
796 817
797 supf1 : Ordinal → Ordinal 818 supf1 : Ordinal → Ordinal
798 supf1 z = ? 819 supf1 z with trio< z x
799 -- ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z 820 ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
821 ... | tri≈ ¬a b ¬c = {!!}
822 ... | tri> ¬a ¬b c = {!!}
800 823
801 pchain : HOD 824 pchain : HOD
802 pchain = UnionCF A f mf ay supf1 x 825 pchain = UnionCF A f mf ay supf1 x
803 826
804 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y 827 pchain⊆A : {y : Ordinal} → odef pchain y → odef A y