# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592092634 -32400
# Node ID 9972bd4a0d6ffb3017ee4b5db03d3327a05cb4e9
# Parent  773e03dfd6ede9a2092799a08e02413aab1f59d7
...

diff -r 773e03dfd6ed -r 9972bd4a0d6f filter.agda
--- 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 )
+