### changeset 267:e469de3ae7cc

author Shinji KONO Mon, 30 Sep 2019 20:59:45 +0900 0d7d6e4da36f 7b4a66710cdd filter.agda 1 files changed, 17 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
```--- a/filter.agda	Mon Sep 30 17:07:40 2019 +0900
+++ b/filter.agda	Mon Sep 30 20:59:45 2019 +0900
@@ -22,36 +22,39 @@
open _∨_
open Bool

+_∩_ : ( A B : OD  ) → OD
+A ∩ B = record { def = λ x → def A x ∧ def B x }
+
+_∪_ : ( A B : OD  ) → OD
+A ∪ B = Union (A , B)
+
record Filter  ( L : OD  ) : Set (suc n) where
field
-       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)
+       F1 : { p q : OD } → L ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → L ∋ q
+       F2 : { p q : OD } → L ∋ p →  L ∋ q  → L ∋ (p ∩ q)

open Filter

proper-filter : {L : OD} → Filter L → Set n
-proper-filter {L} P = ¬ ( def L o∅ )
+proper-filter {L} P = ¬ ( L ∋ od∅ )

-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 )
+prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
+prime-filter {L} P {p} {q} =  L ∋ ( p ∪ q) → ( L ∋ p ) ∨ ( L ∋ q )

-ultra-filter :  {L : OD} → Filter L → {p : Ordinal } → Set n
-ultra-filter {L} P {p} = ( def L p ) ∨ ( ¬ ( def L p ))
+ultra-filter :  {L : OD} → Filter L → {p : OD } → Set n
+ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))

postulate
-   dist-ord : {p q r : Ordinal } → minα p ( maxα q r ) ≡ maxα  ( minα p q ) ( minα p r )
+   dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )

-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 : 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 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 )
+filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim ( y ? )

-generated-filter : {L : OD} → Filter L → (p : Ordinal ) → Filter ( record { def = λ x → def L x ∨ (x ≡ p) } )
+generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
generated-filter {L} P p = record {
F1 = {!!} ; F2 = {!!}
}```