Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1191:d969fc17d049
fix FIP again
| author | kono |
|---|---|
| date | Mon, 27 Feb 2023 08:26:35 +0800 |
| parents | e110b56d8cbe |
| children | 2c35ccd5aadd |
| files | src/Topology.agda |
| diffstat | 1 files changed, 39 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Topology.agda Mon Feb 27 07:29:11 2023 +0800 +++ b/src/Topology.agda Mon Feb 27 08:26:35 2023 +0800 @@ -264,15 +264,20 @@ -- Finite Intersection Property +data Finite-∩ (S : HOD) : Ordinal → Set n where + fin-e : Finite-∩ S o∅ + fin-i : {x : Ordinal } → odef S x → Finite-∩ S (& ( * x , * x )) + fin-∩ : {x y : Ordinal } → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (& (* x ∩ * y)) + record FIP {L : HOD} (top : Topology L) : Set n where field limit : {X : Ordinal } → * X ⊆ CS top - → ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) → Ordinal + → ( { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) → Ordinal is-limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) + → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) → {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip) L∋limit : {X : Ordinal } → (CX : * X ⊆ CS top ) - → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x ) + → ( fip : { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) → {x : Ordinal } → odef (* X) x → odef L (limit CX fip) L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx) @@ -328,18 +333,18 @@ -- then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP) -- it means there is a finite cover -- - finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Subbase (Replace (* X) (λ z → L ＼ z)) o∅ - finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z)) o∅) + finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L → Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅ + finCoverBase {X} ox oc with ODC.p∨¬p O (Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅) ... | case1 sb = sb ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where fip09 : {z : Ordinal } → odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y) → ¬ ( odef (* y) z )) fip09 {z} Lz nc = nc ( P∋cover oc Lz ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ )) -- CX is finite intersection - fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x + fip02 : {x : Ordinal} → Finite-∩ (* (CX ox)) x → o∅ o< x 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 ) *iso b sc )) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬sb (subst₂ (λ j k → Finite-∩ j k ) *iso 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 ( ODC.x∋minimal O L (0<P→ne 0<L) ) ))) fip26 = subst (λ k → odef k (& (L ＼ * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso) @@ -352,9 +357,10 @@ fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *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 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 ) - finCoverSet : {X : Ordinal } → (x : Ordinal) → Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD - finCoverSet {X} x (gi rx) = ( L ＼ * x ) , ( L ＼ * x ) - finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy + finCoverSet : {X : Ordinal } → (x : Ordinal) → Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD + finCoverSet {X} x fin-e = ? + finCoverSet {X} x (fin-i rx) = ( L ＼ * x ) , ( L ＼ * x ) + finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy -- -- this defines finite cover finCover : {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal @@ -362,8 +368,9 @@ -- create Finite-∪ from cex isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp) isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where - fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) - fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where + fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb)) + fip60 x fin-e = ? + fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) where fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x)) fip62 = cong₂ (λ j k → & (j , k )) *iso *iso fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) )) @@ -377,7 +384,7 @@ & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (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 + fip60 x∩y (fin-∩ {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₂ _∪_ *iso *iso ⟩ @@ -386,14 +393,21 @@ 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 ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) (fip70 o∅ (finCoverBase xo xcp)) where - fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) - fip70 x (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } - fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers - (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where + fip70 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x) + fip70 x fin-e = ? + fip70 x (fin-i rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } + fip70 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) ? covers + (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪ (L ＼ b)) fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x) ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ ) ⟫ - ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ + ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx ⟫ + 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 } + fip72 : {a b c : HOD} → a covers c → (b ∪ a) covers c + fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) + ; isCover = isCover cov } fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) ) fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where fip44 : {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal @@ -428,7 +442,7 @@ -- 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 - has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) + has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) → o∅ o< X → ¬ ( Intersection (* X) =h= od∅ ) has-intersection {X} CX fip 0<X i=0 = ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05 ⟫ )) where fp07 : HOD -- we have an element of X @@ -439,12 +453,12 @@ no-cover cov = ⊥-elim ( ? ) where fp01 : Ordinal fp01 = Compact.finCover compact (OOX CX) cov - fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) ) - fp02 t fin-e = gi ? - fp02 t (fin-i tx ) = gi fp03 where + fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Finite-∩ (* X) (& ( L ＼ * t ) ) + fp02 t fin-e = ? + fp02 t (fin-i tx ) = ? where fp03 : odef (* X) (& (L ＼ * t)) fp03 = ? - fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x) (fp02 ty y ) ) where + fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Finite-∩ (* X) k ) fp04 ( fin-∩ (fp02 tx x) (fp02 ty y ) ) where fp04 : & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty))) fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x @@ -497,14 +511,14 @@ & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩ & fp07 <⟨ c<→o< fp08 ⟩ & (* X) ∎ where open o≤-Reasoning O - limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) + limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) → Ordinal limit {X} CX fip with trio< X o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a ) ... | tri≈ ¬a b ¬c = o∅ ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c)) fip00 : {X : Ordinal} (CX : * X ⊆ CS top) - (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) + (fip : {x : Ordinal} → Finite-∩ (* X) x → o∅ o< x) {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip ) fip00 {X} CX fip {x} Xx with trio< X o∅ ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )