# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1569830860 -32400
# Node ID 0d7d6e4da36ff3dd372c1552cfb8ef2845005868
# Parent  9bf100ae50ac8b86059fb2de8b1f03c5cd9ff38b
...

diff -r 9bf100ae50ac -r 0d7d6e4da36f filter.agda
--- a/filter.agda	Mon Sep 30 16:34:15 2019 +0900
+++ b/filter.agda	Mon Sep 30 17:07:40 2019 +0900
@@ -24,24 +24,42 @@
 
 record Filter  ( L : OD  ) : Set (suc n) where
    field
-       F1 : { p q : OD  } → L ∋ p →  od→ord p o< od→ord q  → L ∋ q
-       F2 : { p q : OD  } → L ∋ p →  L ∋ q  → def L (minα (od→ord p ) (od→ord q ))
+       F1 : { p q : Ordinal } → def L p →  p o< osuc q  → def L q
+       F2 : { p q : Ordinal } → def L p →  def L q  → def L (minα p q)
 
 open Filter
 
 proper-filter : {L : OD} → Filter L → Set n
-proper-filter {L} P = ¬ ( L ∋ od∅ )
-
-prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
-prime-filter {L} P {p} {q} =  def L ( maxα ( od→ord p ) (od→ord  q )) → ( L ∋ p ) ∨ ( L ∋ q )
+proper-filter {L} P = ¬ ( def L o∅ )
 
-ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n 
-ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
+prime-filter : {L : OD} → Filter L → {p q : Ordinal } → Set n
+prime-filter {L} P {p} {q} =  def L ( maxα p q) → ( def L p ) ∨ ( def L q )
 
--- H(ω,2) = Lower ( Lower ω ) = Def ( Def ω))
+ultra-filter :  {L : OD} → Filter L → {p : Ordinal } → Set n 
+ultra-filter {L} P {p} = ( def L p ) ∨ ( ¬ ( def L p ))
 
 postulate
    dist-ord : {p q r : Ordinal } → minα p ( maxα q r ) ≡ maxα  ( minα p q ) ( minα p r )
 
-filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : OD } → ( (p : OD) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
-filter-lemma1 {L} P {p} {q} u lt = {!!}
+filter-lemma1 :  {L : OD} → (P : Filter L)  → {p q : Ordinal } → ( (p : Ordinal ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
+filter-lemma1 {L} P {p} {q} u lt with u p | u q
+filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x
+filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y with trio< p q
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri< a ¬b ¬c =  ⊥-elim ( y lt )
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri≈ ¬a refl ¬c = ⊥-elim ( y lt )
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y | tri> ¬a ¬b c = ⊥-elim ( x lt )
+
+generated-filter : {L : OD} → Filter L → (p : Ordinal ) → Filter ( record { def = λ x → def L x ∨ (x ≡ p) } )
+generated-filter {L} P p = record {
+     F1 = {!!} ; F2 = {!!}
+   }
+
+-- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
+
+infinite = ZF.infinite OD→ZF
+
+Hω2 : Filter (Power (Power infinite))
+Hω2 = {!!}
+