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

changeset 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
files src/Tychonoff.agda
diffstat 1 files changed, 15 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Thu Mar 02 12:42:22 2023 +0800
+++ b/src/Tychonoff.agda	Thu Mar 02 18:03:04 2023 +0900
@@ -85,7 +85,7 @@
            * o∅ ≡⟨  o∅≡od∅ ⟩
            od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
    ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → UFLP.limit (uflp (F CSX fip) (ultraf CSX fip)) ; is-limit =  ? } where
+... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  ? } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
@@ -162,10 +162,22 @@
      -- so i has a limit as a limit of UIP
      --
      limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
-     limit {X} CSX fp = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
+     limit {X} CSX fp with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = UFLP.limit ( uflp ( mf CSX fp ) (ultraf CSX fp))
+     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
+           * X ≡⟨ cong (*) (sym 0=X) ⟩
+           * o∅ ≡⟨  o∅≡od∅ ⟩
+           od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
+     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      uf02 : {X v  : Ordinal} → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) 
         → Neighbor TP (limit CSX fp) v → * v ⊆  filter ( mf CSX fp )  
-     uf02 {X} {v} CSX fp nei {x} vx = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf CSX fp)) nei vx
+     uf02 {X} {v} CSX fp nei {x} vx with trio< o∅ X
+     ... | tri< 0<X ¬b ¬c = UFLP.is-limit ( uflp  ( mf CSX fp ) (ultraf CSX fp)) nei vx
+     ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
+           * X ≡⟨ cong (*) (sym 0=X) ⟩
+           * o∅ ≡⟨  o∅≡od∅ ⟩
+           od∅ ∎ ) (sym &iso) ? ) ) where open ≡-Reasoning
+     ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      --
      -- the limit is an limit of entire elements of X
      --