Members/kono/Proof/ZF-in-agda: src/Topology.agda comparison

comparison src/Topology.agda @ 1188:8cbc3918d875

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sun, 26 Feb 2023 11:16:32 +0900
parents	d996fe8dd116
children	0201827b08ac

comparison

equal deleted inserted replaced

-:d996fe8dd116
+:8cbc3918d875
 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)
 -- Compact
 data Finite-∪ (S : HOD) : Ordinal → Set n where
-fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
+fin-e : Finite-∪ S o∅
-fin-∪  : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
+fin-i : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
+fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
 record Compact  {L : HOD} (top : Topology L)  : Set n where
 field
 finCover  : {X : Ordinal } → (* X) ⊆ OS top → (* X) covers L → Ordinal
 isCover   : {X : Ordinal } → (xo : (* X) ⊆ OS top) → (xcp : (* X) covers L ) → (* (finCover xo xcp )) covers L
 fip02 : {x : Ordinal } → ¬ odef L x
 fip02 {x} Lx = ⊥-elim ( o<¬≡ (sym b) (∈∅< Lx) )
 fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L
 fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx)  ; P∋cover = λ Lx → ⊥-elim (fip02 Lx)  ; isCover =  λ Lx → ⊥-elim (fip02 Lx) }
 fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅
-fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) )
+fip00 {X} xo xcp = fin-e
 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
 -- set of coset of X
 CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
-CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+CX {X} ox = & ( Replace (* X) (λ z → L ＼  z ))
 CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top
 CCX {X} os {x} ox with subst (λ k → odef k x) *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))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where
 --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
 --     it means there is a finite cover
 --
 record CFIP (X x : Ordinal) : Set n where
 field
-is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z)
+is-CS : * x ⊆ Replace (* X) (λ z → L ＼ z)
 sx :  Subbase (* x)  o∅
 Cex : (X : Ordinal ) → HOD
-Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L ＼ z))) ; <odmax = fip05 } where
+Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace (* X) (λ z → L ＼ z))) ; <odmax = fip05 } where
-fip05 :  {y : Ordinal} →   CFIP X y → y o< osuc (& (Replace' (* X) (λ z xz → L ＼ z)))
+fip05 :  {y : Ordinal} →   CFIP X y → y o< osuc (& (Replace (* X) (λ z → L ＼ z)))
 fip05 {y} cf = subst₂ (λ j k → j o< osuc k ) &iso refl ( ⊆→o≤ ( CFIP.is-CS cf ) )
 fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ )
 fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
 -- CX is finite intersection
 fip02 : {x : Ordinal} → Subbase (* (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 (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* (CX ox)) k) b sc } )) where
-fip10 : * (CX ox) ⊆ Replace' (* X) (λ z xz → L ＼ z)
+fip10 : * (CX ox) ⊆ Replace (* X) (λ z → L ＼ z)
 fip10 {w} cw = subst (λ k → odef k w) *iso cw
 -- 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)
 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 }
 CXfip : {X : Ordinal } → (ox : * X ⊆ OS top) → (oc : * X covers L) → CFIP X (cex ox oc)
 CXfip {X} ox oc  = ODC.x∋minimal O (Cex X) (fip00 ox oc)
 --
 -- this defines finite cover
 finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
-finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼  z ))
+finCover {X} ox oc = & ( Replace (* (cex ox oc)) (λ z → L ＼  z ))
 -- create Finite-∪ from cex
 isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
 isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where
-fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼  z )))
+fip30 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) →  Subbase (* x) y → Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼  z )))
 fip30 x y x⊆cs (gi sb) = fip31 where
-fip32 : Replace' (* x) (λ z xz → L ＼ z) ⊆ * X --  x⊆cs :* x ⊆ Replace' (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
+fip32 : Replace (* x) (λ z → L ＼ z) ⊆ * X
 fip32 {w} record { z = z ; az = xz ; x=ψz = x=ψz } with x⊆cs xz
 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
 fip34 : * z1 ⊆ L
 fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
 fip33 : z1 ≡ w
 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
 & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
 & (L ＼ * z) ≡⟨ sym x=ψz ⟩
 w ∎ where open ≡-Reasoning
-fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z)))
+--  x⊆cs :* x ⊆ Replace (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
-fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
+fp38 : Subbase (* x) y
+fp38 = gi sb
+fp35 : odef (* x) y
+fp35 = sb
+fp36 : odef (Replace (* X) (λ z → L ＼ z)) y
+fp36 = x⊆cs sb
+fp37 : odef (* X) (& (L ＼ * y))
+fp37 = ?
+fip31 : Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼ z)))
+fip31 = fin-i (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
 fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
-fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L ＼ z₁)))
+fip35 : Finite-∪ (* X) (& (Replace (* x) (λ z₁ → L ＼ z₁)))
 fip35 = subst (λ k → Finite-∪ (* X) k)
-(cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
+(cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace (* x) (λ z₁ → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
 -- 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 ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
 ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
 fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
 ... | case2 Lb = P∋cover cb Lb
 fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x
 fip47 {x} Lab with  fip45 {L} {a} {b} Lab
 ... | case1 La = isCover ca La
 ... | case2 Lb = isCover cb Lb
-fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y
+fip40 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) →  Subbase (* x) y
-→ (Replace' (* x) (λ z xz → L ＼  z )) covers (L ＼ * y )
+→ (Replace (* x) (λ z → L ＼  z )) covers (L ＼ * y )
-fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
+fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace (* x) (λ z → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
 ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where
-fip41 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * a)
+fip41 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * a)
 fip41 = fip40 x a x⊆r sa
-fip42 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * b)
+fip42 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * b)
 fip42 = fip40 x b x⊆r sb
 fip40 x y x⊆r (gi sb) with x⊆r sb
 ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
 fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal
 fip51 {w} Lyw = z
 fip56 = begin
 * z ≡⟨ sym (L＼Lx=x fip55 ) ⟩
 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso)  ⟩
 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz)  ⟩
 L ＼ * y ∎  where open ≡-Reasoning
-fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z
+fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace (* x) (λ z₁ → L ＼ z₁)) z
 fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
 fip54 : z ≡ & ( L ＼ * y )
 fip54 = begin
 z ≡⟨ sym &iso ⟩
 & (* z) ≡⟨ cong (&) fip56 ⟩
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
 ... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? }
 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
 -- set of coset of X
 OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
-OX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+OX {X} ox = & ( Replace (* X) (λ z → L ＼  z ))
 OOX : {X : Ordinal} → (cs :  * X ⊆ CS top) → * (OX cs) ⊆ OS top
 OOX {X} cs {x} ox with subst (λ k → odef k x) *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
 no-cover : ¬ ( (* (OX CX)) covers L )
 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 t⊆OX ) = gi fp03 where
+fp02 t fin-e = gi ?
+fp02 t (fin-i tx ) = gi fp03 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
 fp04 :  & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
 fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where

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

comparison src/Topology.agda @ 1188:8cbc3918d875