Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1485:5dacb669f13b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2024 15:43:35 +0900 |
| parents | 0b30bb7c7501 |
| children | 49c3ef1e9b4f |
| files | src/BAlgebra.agda src/ODUtil.agda src/Topology.agda src/ZProduct.agda |
| diffstat | 4 files changed, 133 insertions(+), 95 deletions(-) [+] |
line wrap: on
line diff
--- a/src/BAlgebra.agda Mon Jul 01 07:00:04 2024 +0900 +++ b/src/BAlgebra.agda Mon Jul 01 15:43:35 2024 +0900 @@ -39,9 +39,9 @@ lem1 : {x : Ordinal} → odef od∅ x → odef (L ＼ L) x lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt )) -＼-cong : (P Q R S : HOD) → P =h= R → Q =h= S → (P ＼ Q) =h= (R ＼ S) -eq→ (＼-cong P Q R S p=r q=s) {x} ⟪ px , npq ⟫ = ⟪ eq→ p=r px , (λ lt → npq (eq← q=s lt) ) ⟫ -eq← (＼-cong P Q R S p=r q=s ) {x} ⟪ rx , nrs ⟫ = ⟪ eq← p=r rx , (λ lt → nrs (eq→ q=s lt) ) ⟫ +＼-cong : (P R Q S : HOD) → P =h= R → Q =h= S → (P ＼ Q) =h= (R ＼ S) +eq→ (＼-cong P R Q S p=r q=s) {x} ⟪ px , npq ⟫ = ⟪ eq→ p=r px , (λ lt → npq (eq← q=s lt) ) ⟫ +eq← (＼-cong P R Q S p=r q=s ) {x} ⟪ rx , nrs ⟫ = ⟪ eq← p=r rx , (λ lt → nrs (eq→ q=s lt) ) ⟫ L＼Lx=x : {x : HOD} → x ⊆ L → (L ＼ ( L ＼ x )) =h= x L＼Lx=x {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 } where
--- a/src/ODUtil.agda Mon Jul 01 07:00:04 2024 +0900 +++ b/src/ODUtil.agda Mon Jul 01 15:43:35 2024 +0900 @@ -54,6 +54,10 @@ eq→ (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq← *iso px , eq← *iso qx ⟫ eq← (*iso∩ {p} {q}) {x} ⟪ px , qx ⟫ = ⟪ eq→ *iso px , eq→ *iso qx ⟫ +∩-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∩ C) =h= (B ∩ D) +eq→ (∩-cong eq1 eq2) {x} lt = ⟪ eq→ eq1 (proj1 lt) , eq→ eq2 (proj2 lt) ⟫ +eq← (∩-cong eq1 eq2) {x} lt = ⟪ eq← eq1 (proj1 lt) , eq← eq2 (proj2 lt) ⟫ + power→⊆ : ( A t : HOD) → Power A ∋ t → t ⊆ A power→⊆ A t PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x)) where t1 : {x : HOD } → t ∋ x → A ∋ x @@ -82,6 +86,12 @@ lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) +∪-cong : {A B C D : HOD} → A =h= B → C =h= D → (A ∪ C) =h= (B ∪ D) +eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq→ eq1 lt) +eq→ (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq→ eq2 lt) +eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case1 lt) = case1 (eq← eq1 lt) +eq← (∪-cong {A} {B} {C} {D} eq1 eq2) {x} (case2 lt) = case2 (eq← eq2 lt) + x∪x≡x : { A : HOD } → (A ∪ A) =h= A x∪x≡x {A} = record { eq← = λ {x} lt → case1 lt ; eq→ = lem00 } where lem00 : {x : Ordinal} → odef A x ∨ odef A x → odef A x
--- a/src/Topology.agda Mon Jul 01 07:00:04 2024 +0900 +++ b/src/Topology.agda Mon Jul 01 15:43:35 2024 +0900 @@ -86,15 +86,15 @@ CS∋L : CS ∋ L CS∋L = ⟪ (λ lt → eq→ *iso lt) , subst (λ k → odef OS k) (sym lem0) OS∋od∅ ⟫ where lem0 : & (L ＼ * (& L)) ≡ & od∅ - lem0 = ==→o≡ ( ==-trans (＼-cong L (* (& L)) L L ==-refl *iso ) L＼L=0 ) + lem0 = ==→o≡ ( ==-trans (＼-cong L L (* (& L)) L ==-refl *iso ) L＼L=0 ) CS⊆PL : CS ⊆ Power L CS⊆PL {x} Cx y xy = proj1 Cx xy P＼CS=OS : {cs : HOD} → CS ∋ cs → OS ∋ ( L ＼ cs ) - P＼CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (==→o≡ (＼-cong L (* (& cs)) L cs ==-refl *iso)) olcs + P＼CS=OS {cs} ⟪ cs⊆L , olcs ⟫ = subst (λ k → odef OS k) (==→o≡ (＼-cong L L (* (& cs)) cs ==-refl *iso)) olcs P＼OS=CS : {cs : HOD} → OS ∋ cs → CS ∋ ( L ＼ cs ) P＼OS=CS {os} oos = ⟪ (λ lt → proj1 (eq→ *iso lt)) , subst (λ k → odef OS k) (==→o≡ (==-sym (==-trans ( - ＼-cong L (* ( & (L ＼ os))) L (L ＼ os) ==-refl *iso ) (L＼Lx=x {os} (os⊆L oos)) ))) oos ⟫ + ＼-cong L L (* ( & (L ＼ os))) (L ＼ os) ==-refl *iso ) (L＼Lx=x {os} (os⊆L oos)) ))) oos ⟫ open Topology @@ -136,7 +136,7 @@ cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc ) cc09 : (L ＼ * (& (L ＼ * c))) =h= (* c) cc09 = begin - L ＼ * (& (L ＼ * c)) ≈⟨ ＼-cong L (* (& (L ＼ * c))) L (L ＼ * c) ==-refl *iso ⟩ + L ＼ * (& (L ＼ * c)) ≈⟨ ＼-cong L L (* (& (L ＼ * c))) (L ＼ * c) ==-refl *iso ⟩ L ＼ (L ＼ * c) ≈⟨ L＼Lx=x {* c} cc08 ⟩ * c ∎ where open EqHOD ==-Setoid @@ -277,17 +277,16 @@ pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q)) - tp01 w wz = ? - -- tp01 w wz with subst (λ k → odef k w ) ? wz - -- ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where - -- tp03 : odef P a - -- tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa + tp01 w wz with eq→ *iso wz + ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where + tp03 : odef P a + tp03 = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa pbase⊆PL {P} {Q} TP TQ {z} (case2 record { q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01 where tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) )) - tp01 w wz = ? -- with subst (λ k → odef k w ) ? wz - -- ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where - -- tp03 : odef Q b - -- tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb + tp01 w wz with eq→ *iso wz + ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 ) where + tp03 : odef Q b + tp03 = os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb pbase : {P Q : HOD} → Topology P → Topology Q → HOD pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where @@ -307,6 +306,12 @@ open _covers_ +cong-covers : (P Q R S : HOD) → P =h= Q → R =h= S → P covers R → Q covers S +cong-covers P Q R S P=Q R=S record { cover = cover ; P∋cover = P∋cover ; isCover = isCover } + = record { cover = λ {x} px → cover (eq← R=S px) ; P∋cover = λ {x} px → eq→ P=Q (P∋cover (eq← R=S px)) + ; isCover = λ {x} px → isCover (eq← R=S px) } + + -- Finite Intersection Property record FIP {L : HOD} (top : Topology L) : Set n where @@ -355,22 +360,24 @@ CX : {X : Ordinal} → * X ⊆ OS top → Ordinal CX {X} ox = & ( Replace (* X) (λ z → L ＼ z ) RC＼ ) CCX : {X : Ordinal} → (os : * X ⊆ OS top) → * (CX os) ⊆ CS top - CCX {X} os {x} ox = ? -- with subst (λ k → odef k x) ? ox - -- ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L ＼ * z) - -- fip07 : z ≡ & (L ＼ * x) - -- fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where - -- fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x - -- fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) ? not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ - -- ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ ) - -- fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) - -- fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , subst (λ k → ¬ odef k w) ? fip10 ⟫ where - -- fip10 : ¬ (odef (L ＼ * z) w) - -- fip10 ⟪ Lw , nzw ⟫ = nzw zw - -- fip06 : odef (OS top) (& (L ＼ * x)) - -- fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) - -- fip05 : * x ⊆ L - -- fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw ) - + CCX {X} os {x} ox with eq→ *iso ox + ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06 ⟫ where -- x ≡ & (L ＼ * z) + fip07 : z ≡ & (L ＼ * x) + fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } ) where + fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x + fip08 {x} ⟪ Lx , not ⟫ = double-neg-elim ( λ nz → not (eq← *iso ⟪ Lx , nz ⟫) ) -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥ + fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) + fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw , (λ lt → fip10 (eq→ *iso lt)) ⟫ where + fip10 : ¬ (odef (L ＼ * z) w) + fip10 ⟪ Lw , nzw ⟫ = nzw zw + fip06 : odef (OS top) (& (L ＼ * x)) + fip06 = os ( subst (λ k → odef (* X) k ) fip07 az ) + fip05 : * x ⊆ L + fip05 {w} xw = proj1 ( eq→ (begin + * x ≈⟨ o≡→== x=ψz ⟩ + * (& ( L ＼ * z )) ≈⟨ *iso ⟩ + L ＼ * z ∎ ) xw ) where + open EqHOD ==-Setoid -- -- X covres L means Intersection of (CX X) contains nothing -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) @@ -387,19 +394,18 @@ fip02 {x} sc with trio< x o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri> ¬a ¬b c = c - ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (subst₂ (λ j k → Subbase j k ) ? b sc )) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (sb⊆ (eq→ *iso) (subst (λ k → Subbase (* (CX ox)) k ) b sc ))) -- we have some intersection because L is not empty (if we have an element of L, we don't need choice) fip26 : odef (* (CX ox)) (& (L ＼ * ( cover oc ( x∋minimal L (0<P→ne 0<L) ) ))) - fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( x∋minimal L (0<P→ne 0<L) ) )) )) ? - record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } + fip26 = eq← *iso record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L)) ; x=ψz = refl } fip25 : odef L( FIP.limit fip (CCX ox) fip02 ) fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26 fip20 : {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 )) fip20 {y} Xy yl = proj2 fip21 yl where fip22 : odef (* (CX ox)) (& ( L ＼ * y )) - fip22 = subst (λ k → odef k (& ( L ＼ * y ))) ? record { z = y ; az = Xy ; x=ψz = refl } + fip22 = eq← *iso record { z = y ; az = Xy ; x=ψz = refl } fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 ) - fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) ? ( FIP.is-limit fip (CCX ox) fip02 fip22 ) + fip21 = eq→ *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) -- create HOD from Subbase ( finite intersection ) finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x → HOD finCoverSet {X} x (gi rx) = ( L ＼ * x ) , ( L ＼ * x ) @@ -414,7 +420,7 @@ fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) - fip62 = cong₂ (λ j k → & (j , k )) ? ? + fip62 = ==→o≡ (pair-subst2 *iso *iso ) fip61 : odef (Replace (* X) (_＼_ L) RC＼ ) x → odef (* X) ( & ((L ＼ * x ) )) fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where fip34 : * z1 ⊆ L @@ -422,26 +428,29 @@ fip33 : z1 ≡ & (L ＼ * x) fip33 = begin z1 ≡⟨ sym &iso ⟩ - & (* z1) ≡⟨ cong (&) ? ⟩ - & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) ? ⟩ + & (* z1) ≡⟨ sym ( ==→o≡ (L＼Lx=x {* z1} fip34)) ⟩ + & (L ＼ ( L ＼ * z1)) ≡⟨ ==→o≡ ( ＼-cong L L ( L ＼ * z1) (* (& ( L ＼ * z1))) ==-refl (==-sym *iso) ) ⟩ & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ & (L ＼ * x ) ∎ where open ≡-Reasoning fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx) (fip60 y sy) ) where fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy) - fip62 = cong (&) ( begin - (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ ? ? ⟩ - finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning + fip62 = ==→o≡ (begin + (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) + ≈⟨ ∪-cong {* (& (finCoverSet x sx))} {finCoverSet x sx} {* (& (finCoverSet y sy))} {finCoverSet y sy} *iso *iso ⟩ + finCoverSet x sx ∪ finCoverSet y sy ∎ ) + where open EqHOD ==-Setoid -- is also a cover isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L - isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) ? (subst (λ k → L ＼ k ≡ L) ? ? ) -- L＼0=L) + isCover1 {X} xo xcp = cong-covers _ _ _ _ (==-sym *iso) (==-trans (＼-cong L L (* o∅) od∅ ==-refl o∅==od∅) L＼0=L) + -- subst₂ (λ j k → j covers k ) ? (subst (λ k → L ＼ k ≡ L) ? ? ) -- L＼0=L) (fip70 o∅ (finCoverBase xo xcp)) where fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) fip70 x (gi rx) = fip73 where fip73 : ((L ＼ * x) , (L ＼ * x)) covers (L ＼ * x) -- obvious fip73 = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl - ; isCover = λ {x} lt → subst (λ k → odef k x) ? lt } - fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers - (L ＼ k)) ? ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where + ; isCover = λ {x} lt → eq← *iso lt } + fip70 x∩y (g∩ {x} {y} sx sy) = cong-covers _ _ _ _ ==-refl (＼-cong L L (* x ∩ * y) (* (& (* x ∩ * y))) ==-refl (==-sym *iso)) + ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where fip71 : {a b c : HOD} → a covers c → (a ∪ b) covers c fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) ; isCover = isCover cov } @@ -467,6 +476,8 @@ ... | case1 La = isCover ca La ... | case2 Lb = isCover cb Lb + + Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top → FIP top Compact→FIP {L} top compact with trio< (& L) o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) @@ -476,18 +487,23 @@ -- if 0 ≡ X then ¬ odef X x fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ({y : Ordinal} → Subbase (* X) y → o∅ o< y) → ¬ odef (* X) x fip000 {X} {x} CX fip xx with trio< o∅ X - ... | tri< 0<X ¬b ¬c = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans ? (cong (*) L=0)) ? ) (sym &iso) - ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) Xe )) where + ... | tri< 0<X ¬b ¬c = ¬∅∋ (eq→ (begin + L ≈⟨ ==-sym *iso ⟩ + * (& L) ≈⟨ o≡→== L=0 ⟩ + * o∅ ≈⟨ o∅==od∅ ⟩ + od∅ ∎ ) (subst (λ k → odef L k ) (sym &iso) + ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx)) Xe ))) where + open EqHOD ==-Setoid 0<x : o∅ o< x 0<x = fip (gi xx ) e : HOD -- we have an element of x e = minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) Xe : odef (* x) (& e) Xe = x∋minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) ) - ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin - * X ≡⟨ cong (*) (sym 0=X) ⟩ - * o∅ ≡⟨ ? ⟩ - od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning + ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (eq→ ( begin + * X ≈⟨ o≡→== (sym 0=X) ⟩ + * o∅ ≈⟨ o∅==od∅ ⟩ + od∅ ∎ ) (subst (λ k → odef (* X) k ) (sym &iso) xx ) )) where open EqHOD ==-Setoid ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where -- set of coset of X @@ -495,13 +511,13 @@ OX : {X : Ordinal} → * X ⊆ CS top → Ordinal OX {X} ox = & ( Replace (* X) (λ z → L ＼ z ) RC＼) OOX : {X : Ordinal} → (cs : * X ⊆ CS top) → * (OX cs) ⊆ OS top - OOX {X} cs {x} ox = ? -- with subst (λ k → odef k x) ? ox - -- ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where - -- comp01 : odef (* X) (& (* z)) - -- comp01 = subst (λ k → odef (* X) k) (sym &iso) az - -- if all finite intersection of X contains something, - -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) - -- it means there is a limit + OOX {X} cs {x} ox with eq→ *iso ox + ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01)) where + comp01 : odef (* X) (& (* z)) + comp01 = subst (λ k → odef (* X) k) (sym &iso) az + -- if all finite intersection of X contains something, + -- there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact) + -- it means there is a limit record NC {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) (0<X : o∅ o< X) : Set n where field -- find an element x, which is not covered (which is a limit point) x : Ordinal @@ -529,43 +545,52 @@ fp22 : e ⊆ L fp22 {x} lt = cs⊆L top (CX Xe) lt fp21 : & e ≡ & (L ＼ * (& (L ＼ e))) - fp21 = cong (&) (trans (sym ?) (cong (λ k → L ＼ k) ?)) + fp21 = ==→o≡ ( ==-trans (==-sym (L＼Lx=x {e} fp22 )) (＼-cong L L (L ＼ e) (* (& (L ＼ e))) ==-refl (==-sym *iso ))) fp23 : (L ＼ * (& (L ＼ e))) ⊆ (L ＼ Union (* o∅)) - fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ? (sym &iso) (Own.ao lt )))) ⟫ + fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (eq→ (begin + (* o∅) ≈⟨ o∅==od∅ ⟩ + od∅ ∎ ) (subst (λ k → odef (* o∅) k ) (sym &iso) (Own.ao lt ))))) ⟫ + where open EqHOD ==-Setoid fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03 ; t⊆i = fp24 } where -- we have a single cover x, L ＼ * x is single finite intersection fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x)))) - fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) ? fp25 ⟫ where - fp25 : ¬ odef (Union (* x , * x)) y - fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) ? ox ) - fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) ? ox ) + fp24 {y} ⟪ Lx , not ⟫ = ⟪ Lx , fp26 ⟫ where + fp26 : ¬ odef (Union (* (& (* x , * x)))) y + fp26 record { owner = owner ; ao = ao ; ox = ox } with eq→ *iso ao + ... | case1 refl = not (eq→ *iso ox ) + ... | case2 refl = not (eq→ *iso ox ) fp03 : odef (* X) (& (L ＼ * x)) -- becase x is an element of Replace (* X) (λ z → L ＼ z ) - fp03 = ? -- with subst (λ k → odef k x ) ? tx - -- ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where - -- fip34 : * z1 ⊆ L - -- fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 - -- fip33 : z1 ≡ & (L ＼ * x) - -- fip33 = begin - -- z1 ≡⟨ sym &iso ⟩ - -- & (* z1) ≡⟨ cong (&) (sym (L＼Lx=x fip34 )) ⟩ - -- & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) ? ⟩ - -- & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩ - -- & (L ＼ * x ) ∎ where open ≡-Reasoning + fp03 with eq→ *iso tx + ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where + fip34 : * z1 ⊆ L + fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1 + fip33 : z1 ≡ & (L ＼ * x) + fip33 = trans (sym &iso ) (==→o≡ ( begin + (* z1) ≈⟨ ==-sym (L＼Lx=x {* z1} fip34 ) ⟩ + (L ＼ ( L ＼ * z1)) ≈⟨ ＼-cong L L ( L ＼ * z1) (* x) ==-refl (==-trans (==-sym *iso) (o≡→== (sym x=ψz1)) ) ⟩ + (L ＼ * x ) ∎ ) ) where open EqHOD ==-Setoid fp02 t (fin-∪ {tx} {ty} ux uy ) = record { i = & (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ; sb = fp11 ; t⊆i = fp35 } where fp35 : (L ＼ * (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty)))) - fp35 = subst₂ (λ j k → (L ＼ j ) ⊆ (L ＼ Union k)) ? ? fp36 where + fp35 = λ lt → eq← fp42 ( fp36 (eq→ ( ＼-cong L L (* (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) + (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ==-refl *iso ) lt ) ) where + fp43 : (P : HOD ) → Union (* (& P)) =h= Union P + eq← (fp43 P) record { owner = owner ; ao = ao ; ox = ox } = record { owner = owner ; ao = eq← *iso ao ; ox = ox } + eq→ (fp43 P) record { owner = owner ; ao = ao ; ox = ox } = record { owner = owner ; ao = eq→ *iso ao ; ox = ox } + fp42 : ( L ＼ Union (* (& (* tx ∪ * ty)))) =h= (L ＼ Union (* tx ∪ * ty)) + eq→ fp42 {x} ⟪ lx , nux ⟫ = ⟪ lx , (λ lt → nux (eq← (fp43 _) lt) ) ⟫ + eq← fp42 {x} ⟪ lx , nux ⟫ = ⟪ lx , (λ lt → nux (eq→ (fp43 _) lt) ) ⟫ fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } - = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ? (sym &iso) ao )) - fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) ? uz) where + = ⊥-elim ( ¬∅∋ (eq→ o∅==od∅ (subst (λ k → odef (* o∅) k ) (sym &iso) ao ))) + fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (eq→ (fp43 _) uz) where fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z fp41 x record { owner = .(& (* w)) ; ao = (case1 refl) ; ox = ox } = - os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) ? ox ) + os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (eq→ *iso ox ) fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } = - os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) ? ox ) - fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz = ? -- with subst (λ k → odef (Union k) z ) ? uz - -- ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } - -- ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } + os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (eq→ *iso ox ) + fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with eq→ (fp43 _ ) uz + ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } + ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } fp36 : (L ＼ (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* tx ∪ * ty)) fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where fp37 : ¬ odef (Union (* tx ∪ * ty)) z @@ -573,7 +598,8 @@ fp38 : (L ＼ (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx)) fp38 = SB.t⊆i (fp02 tx ux) fp39 : Union (* tx) ⊆ (* (SB.i (fp02 tx ux))) - fp39 {w} txw = ? -- with ∨L＼X {L} {* (SB.i (fp02 tx ux))} (fp40 ux txw) + fp39 {w} txw with ∨L＼X {L} {(SB.i (fp02 tx ux))} (fp40 ux ?) + ... | t = ? -- ... | case1 sb = sb -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw ) fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where @@ -584,16 +610,16 @@ -- ... | case1 sb = sb -- ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw ) fp04 : {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) - fp04 {tx} {ty} = ? where -- cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where + fp04 {tx} {ty} = ==→o≡ record { eq→ = fp05 ; eq← = fp09 } where fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x - fp05 {x} lt = ? -- with subst₂ (λ j k → odef (j ∩ k) x ) ? ? lt - -- ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) ? ⟪ Lx , fp06 ⟫ where - -- fp06 : ¬ odef (* tx ∪ * ty) x - -- fp06 (case1 tx) = ¬tx tx - -- fp06 (case2 ty) = ¬ty ty + fp05 {x} lt with eq← *iso∩ lt + ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = eq→ (＼-cong L L (* tx ∪ * ty) (* (& (* tx ∪ * ty))) ==-refl (==-sym *iso) ) ⟪ Lx , fp06 ⟫ where + fp06 : ¬ odef (* tx ∪ * ty) x + fp06 (case1 tx) = ¬tx tx + fp06 (case2 ty) = ¬ty ty fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x - fp09 {x} lt with subst (λ k → odef (L ＼ k) x) ? lt - ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) ? ? + fp09 {x} lt with eq→ (＼-cong L L (* (& (* tx ∪ * ty))) (* tx ∪ * ty) ==-refl *iso ) lt + ... | ⟪ Lx , ¬tx∨ty ⟫ = eq→ *iso∩ ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty)) ⟫ ⟫ fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))))) fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx ux)) (SB.sb (fp02 ty uy )) ) @@ -711,4 +737,3 @@ -
--- a/src/ZProduct.agda Mon Jul 01 07:00:04 2024 +0900 +++ b/src/ZProduct.agda Mon Jul 01 15:43:35 2024 +0900 @@ -76,6 +76,9 @@ eq← (proj2 (pair-subst {x} {y} {z} x=y)) {w} (case1 wz) = case1 wz eq← (proj2 (pair-subst {x} {y} {z} x=y)) {w} (case2 wy) = case2 (trans wy (sym ( ==→o≡ x=y))) +pair-subst2 : { x y z w : HOD } → x =h= y → z =h= w → ( (x , z ) =h= ( y , w )) +pair-subst2 x=y z=w = ==-trans (proj1 (pair-subst x=y) ) (proj2 (pair-subst z=w)) + -- We don't have this but x =h= y ( ord→== ) -- ord≡→== : { x y : HOD } → & x ≡ & y → x ≡ y -- ord≡→== eq = ? -- subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )