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

diff -r ef93c56ad311 -r 773e03dfd6ed filter.agda
--- a/filter.agda	Fri Jun 12 19:21:14 2020 +0900
+++ b/filter.agda	Sat Jun 13 15:59:10 2020 +0900
@@ -33,32 +33,37 @@
 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
        filter : OD   
-       ¬f∋∅ : ¬ ( filter ∋ od∅ )
-       f∋L :  filter ∋ L
        f⊆PL :  filter ⊆ Power L 
        filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
        filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
+open Filter
+
+proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
+proper-filter {L} P {p} = filter P ∋ L
+
+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∋∅ : ideal ∋ od∅ 
-       ¬i∋L : ¬ ( ideal ∋ L )
        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 Filter
 open Ideal
 
-L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
-L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!}
+proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
+proper-ideal {L} P {p} = ideal 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 )
+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) )