# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1592182398 -32400
# Node ID 822b50091a2665078fe320ae7299a5fd50c976a9
# Parent  4340ffcfa83d2e77957090e082c011f73c6c332f
fix prime

diff -r 4340ffcfa83d -r 822b50091a26 filter.agda
--- a/filter.agda	Sun Jun 14 19:11:38 2020 +0900
+++ b/filter.agda	Mon Jun 15 09:53:18 2020 +0900
@@ -28,7 +28,7 @@
 open _∨_
 open Bool
 
--- Kunen p.76 and p.53 
+-- Kunen p.76 and p.53, we use ⊆
 record Filter  ( L : OD  ) : Set (suc n) where
    field
        filter : OD   
@@ -38,12 +38,15 @@
 
 open Filter
 
--- should use inhabit?
-proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
-proper-filter {L} P {p} = ¬ (filter P ∋ od∅)
+record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       prime   : {p q : OD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
 
-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 ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       ultra   : {p : OD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
 
 open _⊆_
 
@@ -67,20 +70,20 @@
 q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
--- is-∅ : ( x : OD ) → Dec ( x ≡ od∅  )
--- is-∅ x with is-o∅ (od→ord x)
--- ... | yes eq = yes {!!}
--- ... | no ne = no {!!}
+-----
+--
+--  ultra filter is prime
+--
 
-record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
-   field
-       proper  : ¬ (filter P ∋ od∅)
-       ultra   : {p : OD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
-
-filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ultra-filter P  → prime-filter {L} P {p} {q}
-filter-lemma1 {L} P {p} {q} u lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
-... | case1 p∈P  = case1 p∈P
-... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
+filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ultra-filter P  → prime-filter P 
+filter-lemma1 {L} P u = record {
+         proper = ultra-filter.proper u
+       ; prime = lemma3
+    } where
+  lemma3 : {p q : OD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+  lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
+  ... | case1 p∈P  = case1 p∈P
+  ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
     lemma5 : ((p ∪ q ) ∩ (L ＼ p)) ==  (q ∩ (L ＼ p))
     lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt  }
        ;  eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
@@ -96,8 +99,13 @@
     lemma8 : (q ∩ (L ＼ p)) ⊆ q
     lemma8 = q∩q⊆q
 
-filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter P
-filter-lemma2 {L} P prime p = {!!}
+-----
+--
+--  if Filter contains L, prime filter is ultra
+--
+
+filter-lemma2 :  {L : OD} → (P : Filter L)  → prime-filter P → ultra-filter P
+filter-lemma2 {L} P prime  = {!!}
 
 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
 generated-filter {L} P p = {!!}