--- a/generic-filter.agda	Sat Jul 25 16:45:22 2020 +0900
+++ b/generic-filter.agda	Sat Jul 25 17:36:27 2020 +0900
@@ -40,7 +40,7 @@
 --
 --
 
-open import Data.List 
+open import Data.List hiding (filter)
 open import Data.Maybe 
 
 import OPair
@@ -60,29 +60,9 @@
      extend : {x : Nat} → (fr : dom f (lift x) ) →  dom g (lift x  )
      feq : {x : Nat} → {fr : dom f (lift x) } →  pmap f (lift x) fr ≡ pmap g (lift x) (extend fr)
 
-record FiniteF (p :  PFunc (Lift n Nat) (Lift n Two) ) : 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 : {n : Level} → F-Dense (PFunc {n}) (λ x → Lift (suc n) (One {n})) _f⊆_ _f∩_
--- Dense-Gf = record {
---        dense =  λ x → FiniteF x
---     ;  d⊆P = lift OneObj
---     ;  dense-f = λ x → record { dom = {!!} ; pmap = {!!} }
---     ;  dense-d = λ {p} d → {!!}
---     ;  dense-p = λ {p} d → {!!}
---   }
-
 open _f⊆_ 
 open import Data.Nat.Properties
 
-
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
@@ -144,14 +124,6 @@
 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
 
--- the set of finite partial functions from ω to 2
-
-Hω2f : Set (suc n)
-Hω2f = (Nat → Set n) → Two
-
-Hω2f→Hω2 : Hω2f  → HOD
-Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }
-
 
 record CountableOrdinal : Set (suc (suc n)) where
    field
@@ -208,3 +180,32 @@
       genf = record { filter = PDHOD C P ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
     ; generic = λ D → {!!}
    }
+
+open GenericFilter
+open Filter
+
+record Incompatible  (P : HOD ) : Set (suc (suc n)) where
+   field
+      except : HOD → ( HOD ∧ HOD )
+      incompatible : { p : HOD } →  P ∋ p  →  P ∋ proj1 (except p )  →  P ∋ proj2 (except p ) 
+          → ( p ⊆ proj1 (except p)  ) ∧ ( p ⊆ proj2 (except p)  )
+          → ∀ ( r : HOD ) →  P ∋ r → ¬ (( proj1 (except p)  ⊆ r ) ∧ ( proj2 (except p)  ⊆ r ))
+
+lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) →  mhod M ∋ P
+    →  Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P )))
+lemma725 = {!!}
+
+lemma725-1 :   Incompatible HODω2
+lemma725-1 = {!!}
+
+lemma726 :  (C : CountableOrdinal) (P : HOD ) 
+    →  Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
+lemma726 = {!!}
+
+--
+--   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
+--
+
+
+
+

--- a/partfunc.agda	Sat Jul 25 16:45:22 2020 +0900
+++ b/partfunc.agda	Sat Jul 25 17:36:27 2020 +0900
@@ -8,7 +8,7 @@
 open import logic
 open import Relation.Binary 
 open import Data.Empty 
-open import Data.List 
+open import Data.List hiding (filter)
 open import Data.Maybe  
 open import Relation.Binary
 open import Relation.Binary.Core