### changeset 293:9972bd4a0d6f

...
author Shinji KONO Sun, 14 Jun 2020 08:57:14 +0900 773e03dfd6ed 4340ffcfa83d filter.agda 1 files changed, 28 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
```--- a/filter.agda	Sat Jun 13 15:59:10 2020 +0900
+++ b/filter.agda	Sun Jun 14 08:57:14 2020 +0900
@@ -13,6 +13,9 @@
open import Relation.Binary.Core
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
+import BAlgbra
+
+open BAlgbra O

open inOrdinal O
open OD O
@@ -23,16 +26,6 @@
open _∨_
open Bool

-_∩_ : ( A B : OD  ) → OD
-A ∩ B = record { def = λ x → def A x ∧ def B x }
-
-_∪_ : ( A B : OD  ) → OD
-A ∪ B = record { def = λ x → def A x ∨ def B x }
-
-_＼_ : ( A B : OD  ) → OD
-A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
-
-
-- Kunen p.76 and p.53
record Filter  ( L : OD  ) : Set (suc n) where
field
@@ -43,44 +36,25 @@

open Filter

+-- should use inhabit?
proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
-proper-filter {L} P {p} = filter P ∋ L
+proper-filter {L} P {p} = ¬ (filter P ∋ od∅)

prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

-record Ideal  ( L : OD  ) : Set (suc n) where
-   field
-       ideal : OD
-       i⊆PL :  ideal ⊆ Power L
-       ideal1 : { p q : OD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
-       ideal2 : { p q : OD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
-
-open Ideal
-
-proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
-proper-ideal {L} P {p} = ideal P ∋ od∅
-
-prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
-prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
-
-
-ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set n
-ultra-filter {L} P {p} = L ∋ p →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
-
+ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set (suc n )
+ultra-filter {L} P {p} = p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )

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-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p}
-filter-lemma2 {L} P prime p with prime {!!}
+filter-lemma1 {L} P {p} {q} u lt with lt
... | t = {!!}

+filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p}
+filter-lemma2 {L} P prime 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 {
-     filter = {!!}  ;
-     filter1 = {!!} ; filter2 = {!!}
-   }
+generated-filter {L} P p = {!!}

record Dense  (P : OD ) : Set (suc n) where
field
@@ -102,3 +76,19 @@
Hω2 : Filter (Power (Power infinite))
Hω2 = {!!}

+
+record Ideal  ( L : OD  ) : Set (suc n) where
+   field
+       ideal : OD
+       i⊆PL :  ideal ⊆ Power L
+       ideal1 : { p q : OD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       ideal2 : { p q : OD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
+
+open Ideal
+
+proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
+proper-ideal {L} P {p} = ideal P ∋ od∅
+
+prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
+prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
+```