--- a/filter.agda	Mon Jul 20 17:22:16 2020 +0900
+++ b/filter.agda	Tue Jul 21 02:19:07 2020 +0900
@@ -127,7 +127,7 @@
 record Dense  (P : HOD ) : Set (suc n) where
    field
        dense : HOD
-       incl :  dense ⊆ Power P 
+       d⊆P :  dense ⊆ Power P 
        dense-f : HOD → HOD
        dense-d :  { p : HOD} → p ⊆ P → dense ∋ dense-f p  
        dense-p :  { p : HOD} → p ⊆ P → p ⊆ (dense-f p) 
@@ -147,32 +147,6 @@
 prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
--------
---    the set of finite partial functions from ω to 2
---
---
-
-import OPair
-open OPair O
-
-data Two : Set n where
-   i0 : Two
-   i1 : Two
-
-record PFunc : Set (suc n) where
-   field
-      restrict : Nat → Set n
-      map : (x : Nat ) → restrict x → Two
-
-open PFunc
-
-record _f⊆_ (f g : PFunc) : Set (suc n) where
-  field
-     extend : (x : Nat) → (fr : restrict f x ) →  restrict g x  
-     feq : (x : Nat) → (fr : restrict f x ) →  map f x fr ≡ map g x (extend x fr)
-
-open _f⊆_
-
 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
        filter : L → Set n
@@ -188,22 +162,110 @@
      ; filter2 = λ {p} {q} f∋p f∋q  → lift ( filter2 f (lower f∋p) (lower f∋q)) 
     }
 
+record F-Dense {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
+   field
+       dense : L → Set n
+       d⊆P :  PL dense 
+       dense-f : L → L 
+       dense-d :  { p : L} → PL (λ x → p ⊆ x ) → dense ( dense-f p  )
+       dense-p :  { p : L} → PL (λ x → p ⊆ x ) → p ⊆ (dense-f p) 
+
+Dense-is-F : {L : HOD} → (f : Dense L ) → F-Dense HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
+Dense-is-F {L} f = record {
+       dense =  λ x → Lift (suc n) ((dense f) ∋ x)
+    ;  d⊆P = λ x f∋x →  power→⊆ _ _ (incl ( d⊆P f  ) (lower f∋x ))
+    ;  dense-f = λ x → dense-f f x
+    ;  dense-d = λ {p} d → lift ( dense-d f (d p refl-⊆ ) )
+    ;  dense-p = λ {p} d → dense-p f (d p refl-⊆) 
+  } where open Dense
+
+-------
+--    the set of finite partial functions from ω to 2
+--
+--
+
+data Two : Set n where
+   i0 : Two
+   i1 : Two
+
+data Three : Set n where
+   j0 : Three
+   j1 : Three
+   j2 : Three
+
+open import Data.List hiding (map)
+
+import OPair
+open OPair O
+
+record PFunc : Set (suc n) where
+   field
+      dom : Nat → Set n
+      map : (x : Nat ) → dom x → Two
+      meq : {x : Nat } → { p q : dom x } → map x p ≡ map x q
+
+open PFunc
+
+data Findp : List Three → (x : Nat) → Set n where
+   v0 : {n : List Three} → Findp ( j0 ∷ n ) Zero
+   v1 : {n : List Three} → Findp ( j1 ∷ n ) Zero
+   vn : {n : List Three} {d : Three} → {x : Nat} → Findp n x → Findp (d ∷ n) (Suc x) 
+
+FPFunc→PFunc : List Three → PFunc
+FPFunc→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → feq fp } where
+     findp : List Three → (x : Nat) → Set n 
+     findp n x = Findp n x
+     find : (n : List Three ) → (x : Nat) → Findp n x → Two
+     find (j0 ∷ _) 0 v0 = i0
+     find (j1 ∷ _) 0 v1 = i1
+     find (d ∷ n) (Suc x) (vn {n} {d} {x} p) = find n x p 
+     feq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
+     feq n {0} {v0} {v0} = refl
+     feq n {0} {v1} {v1} = refl
+     feq [] {Suc x} {()}
+     feq (_ ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) {!!} {!!}  (feq n {x} {p} {q})
+
+record _f⊆_ (f g : PFunc) : Set (suc n) where
+  field
+     extend : {x : Nat} → (fr : dom f x ) →  dom g x  
+     feq : {x : Nat} → {fr : dom f x } →  map f x fr ≡ map g x (extend fr)
+
+open _f⊆_
+
 min  = Data.Nat._⊓_
 -- m≤m⊔n  = Data.Nat._⊔_
 open import Data.Nat.Properties
 
 _f∩_ : (f g : PFunc) → PFunc
-f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
-              ; map = λ x p →  map f x (proj1 p) }
+f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → map f x fr ≡ map g x gr)
+              ; map = λ x p →  map f x (proj1 p) ; meq = meq f }
 
 _↑_ : (Nat → Two) → Nat → PFunc
-f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
+f ↑ i = record { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl }
 
 record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
    field
      gn  : Nat
      f<n :  (f ↑ gn) f⊆ p
 
+record FiniteF  (p : PFunc ) : Set (suc n) where
+   field
+     f-max :  Nat 
+     f-func :  Nat → Two
+     f-p⊆f :  p f⊆ (f-func ↑ f-max)
+     f-f⊆p :  (f-func ↑ f-max) f⊆ p 
+
+open FiniteF
+
+Dense-Gf : F-Dense PFunc (λ x → Lift (suc n) One) _f⊆_ _f∩_
+Dense-Gf = record {
+       dense =  λ x → FiniteF x
+    ;  d⊆P = lift OneObj
+    ;  dense-f = λ x → record { dom = {!!} ; map = {!!} }
+    ;  dense-d = λ {p} d → {!!}
+    ;  dense-p = λ {p} d → {!!}
+  }
+
 open Gf
 
 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
@@ -214,13 +276,47 @@
      ; filter2 = λ {p} {q} fp fq  → record { gn = min (gn fp) (gn fq) ; f<n = f2 fp fq }
  } where
      f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → (f ↑ gn fp) f⊆ q
-     f1 {p} {q} fp p⊆q = record { extend = λ x x<g → extend p⊆q x (extend (f<n fp ) x x<g) ; feq = λ x fr → {!!} } where
+     f1 {p} {q} fp p⊆q = record { extend = λ {x} x<g → extend p⊆q  (extend (f<n fp )  x<g) ; feq = λ {x} {fr} → lemma {x} {fr}  } where
+         lemma : {x : Nat} {fr : Lift n (x ≤ gn fp)} → map (f ↑ gn fp) x fr ≡ map q x (extend p⊆q (extend (f<n fp) fr))
+         lemma {x} {fr} = begin
+             map (f ↑ gn fp) x fr
+            ≡⟨ feq (f<n fp )  ⟩
+             map p x (extend (f<n fp)  fr)
+            ≡⟨ feq p⊆q  ⟩
+             map q x (extend p⊆q  (extend (f<n fp)  fr))
+            ∎  where open ≡-Reasoning 
      f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
-     f2 {p} {q} fp fq  = record { extend = λ  x x<g → record {
-           proj1 = extend (f<n fp ) x (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _)))
-         ; proj2 = record {proj1 = extend (f<n fq ) x (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _)))
-         ;                 proj2 = {!!} }}  ;
-        feq = λ x fr → {!!} } where
+     f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
+            fmin =  f ↑  (min (gn fp) (gn fq)) 
+            lemma1 : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p x) (gr : dom q x) → map p x fr ≡ map q x gr
+            lemma1 {x} x<g fr gr = begin
+                   map p x fr 
+                ≡⟨ meq p ⟩
+                   map p x (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
+                ≡⟨ sym (feq (f<n fp)) ⟩
+                   map (f ↑  (min (gn fp) (gn fq))) x x<g
+                ≡⟨ feq (f<n fq) ⟩
+                   map q x (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
+                ≡⟨ meq q ⟩
+                   map q x gr
+                ∎  where open ≡-Reasoning 
+            lemma2  : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) x
+            lemma2 x<g = record { proj1 = extend (f<n fp ) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))) ;
+                     proj2 = record {proj1 = extend (f<n fq ) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))) ; proj2 = lemma1 x<g }}
+            f∩→⊆ : (p q : PFunc ) → (p f∩ q ) f⊆ q
+            f∩→⊆ p q = record {
+                   extend = λ {x} pq → proj1 (proj2 pq)
+                 ; feq = λ {x} {fr} → (proj2 (proj2 fr)) (proj1 fr) (proj1 (proj2 fr)) 
+                }
+            lemma3 :  {x : Nat}  → ( fr : Lift n (x ≤ min (gn fp) (gn fq)))  → map (f ↑ min (gn fp) (gn fq)) x fr ≡ map (p f∩ q) x (lemma2 fr)
+            lemma3 {x} fr = 
+                  map (f ↑ min (gn fp) (gn fq)) x fr
+                ≡⟨ feq (f<n fq) ⟩
+                  map q x (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
+                ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} )   ⟩
+                  map (p f∩ q) x (lemma2 fr)
+                ∎  where open ≡-Reasoning 
+
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
@@ -255,7 +351,7 @@
     ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
 
 ω→2 : HOD
-ω→2 = Replace (Power infinite) (λ p p⊆i → Replace infinite (λ x i∋x → < x , repl p x > )) where
+ω→2 = Replace (Power infinite) (λ p  → Replace infinite (λ x → < x , repl p x > )) where
   repl : HOD → HOD → HOD
   repl p x with ODC.∋-p O p x
   ... | yes _  = nat→ω 1