--- a/filter.agda	Mon Oct 07 01:28:11 2019 +0900
+++ b/filter.agda	Mon Dec 30 23:45:59 2019 +0900
@@ -110,8 +110,8 @@
    field
        filter : OD
        proper : ¬ ( filter ∋ od∅ )
-       inL : { x : OD} → _⊆_ filter L {x}
-       filter1 : { p q : OD } → ( {x : OD} → _⊆_ q L {x} ) → filter ∋ p →  ({ x : OD} → _⊆_ p q {x} ) → filter ∋ q
+       inL :  filter ⊆ 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
@@ -135,6 +135,7 @@
 
 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 {
+     proper = {!!} ; 
      filter = {!!}  ; inL = {!!} ; 
      filter1 = {!!} ; filter2 = {!!}
    }
@@ -142,9 +143,9 @@
 record Dense  (P : OD ) : Set (suc n) where
    field
        dense : OD
-       incl : { x : OD} → _⊆_ dense P {x}
+       incl :  dense ⊆ P 
        dense-f : OD → OD
-       dense-p :  { p x : OD} → P ∋ p  → _⊆_ p (dense-f p) {x} 
+       dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p) 
 
 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))