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

comparison src/Tychonoff.agda @ 1203:2f09ce1dd2a1

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 Thu, 02 Mar 2023 18:03:04 +0900
parents d6781ad8149e
children 4d894c166762
comparison
equal deleted inserted replaced
1202:d6781ad8149e 1203:2f09ce1dd2a1
83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin 83 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
84 * X ≡⟨ cong (*) (sym 0=X) ⟩ 84 * X ≡⟨ cong (*) (sym 0=X) ⟩
85 * o∅ ≡⟨ o∅≡od∅ ⟩ 85 * o∅ ≡⟨ o∅≡od∅ ⟩
86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning 86 od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c ) 87 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → UFLP.limit (uflp (F CSX fip) (ultraf CSX fip)) ; is-limit = ? } where 88 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit = ? } where
89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n 89 fip : {X : Ordinal} → * X ⊆ CS TP → Set n
90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x 90 fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD 91 N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P) 92 N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) } 93 ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt)) }
160 ultraf {X} CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp) 160 ultraf {X} CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc CSX fp) (proper CSX fp)
161 -- 161 --
162 -- so i has a limit as a limit of UIP 162 -- so i has a limit as a limit of UIP
163 -- 163 --
164 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal 164 limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
165 limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) 165 limit {X} CSX fp with trio< o∅ X
166 ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
167 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
168 * X ≡⟨ cong (*) (sym 0=X) ⟩
169 * o∅ ≡⟨ o∅≡od∅ ⟩
170 od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
171 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
166 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 172 uf02 : {X v : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX)
167 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp ) 173 → Neighbor TP (limit CSX fp) v → * v ⊆ filter ( mf CSX fp )
168 uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx 174 uf02 {X} {v} CSX fp nei {x} vx with trio< o∅ X
175 ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp ( mf CSX fp ) (ultraf CSX fp)) nei vx
176 ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
177 * X ≡⟨ cong (*) (sym 0=X) ⟩
178 * o∅ ≡⟨ o∅≡od∅ ⟩
179 od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
180 ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
169 -- 181 --
170 -- the limit is an limit of entire elements of X 182 -- the limit is an limit of entire elements of X
171 -- 183 --
172 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp) 184 uf01 : {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
173 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp)) 185 uf01 {X} CSX fp {x} xx with ODC.∋-p O (* x) (* (limit CSX fp))