# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595309667 -32400
# Node ID d2cb5278e46d9ea615e7604b4dfda8167fa52fc6
# Parent  0a116938a564c0ebe8042a9fcc7873765fd7356c
...

diff -r 0a116938a564 -r d2cb5278e46d OD.agda
--- a/OD.agda	Tue Jul 21 02:39:09 2020 +0900
+++ b/OD.agda	Tue Jul 21 14:34:27 2020 +0900
@@ -76,7 +76,7 @@
 --
 --  ==→o≡ is necessary to prove axiom of extensionality.
 
-data One : Set n where
+data One {n : Level } : Set n where
   OneObj : One
 
 -- Ordinals in OD , the maximum
diff -r 0a116938a564 -r d2cb5278e46d filter.agda
--- a/filter.agda	Tue Jul 21 02:39:09 2020 +0900
+++ b/filter.agda	Tue Jul 21 14:34:27 2020 +0900
@@ -184,11 +184,11 @@
 --
 --
 
-data Two : Set n where
+data Two : Set where
    i0 : Two
    i1 : Two
 
-data Three : Set n where
+data Three : Set where
    j0 : Three
    j1 : Three
    j2 : Three
@@ -198,7 +198,7 @@
 import OPair
 open OPair O
 
-record PFunc : Set (suc n) where
+record PFunc {n : Level} : Set (suc n) where
    field
       dom : Nat → Set n
       map : (x : Nat ) → dom x → Two
@@ -206,53 +206,279 @@
 
 open PFunc
 
-data Findp : List Three → (x : Nat) → Set n where
+data Findp : List Three → (x : Nat) → Set 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 
-     lemma : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
-     lemma j0 n {x} {p} = refl
-     lemma j1 n {x} {p} = refl
-     lemma j2 n {x} {p} = refl
-     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 (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (lemma h n) (lemma h n) (feq n {x} {p} {q})
+findp : List Three → (x : Nat) → Set 
+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 
+
+Findp=n : (h : Three) → (n : List Three) → {x : Nat} {p : Findp n x } → find n x p ≡ find (h ∷ n) (Suc x) (vn p)
+Findp=n j0 n {x} {p} = refl
+Findp=n j1 n {x} {p} = refl
+Findp=n j2 n {x} {p} = refl
+
+findpeq : (n : List Three) → {x : Nat} {p q : Findp n x } → find n x p ≡ find n x q
+findpeq n {0} {v0} {v0} = refl
+findpeq n {0} {v1} {v1} = refl
+findpeq [] {Suc x} {()}
+findpeq (h ∷ n) {Suc x} {vn p} {vn q} = subst₂ (λ j k → j ≡ k ) (Findp=n h n) (Findp=n h n) (findpeq n {x} {p} {q})
+
+3List→PFunc : List Three → PFunc
+3List→PFunc fp = record { dom = λ x → findp fp x ; map = λ x p → find fp x p ; meq = λ {x} {p} {q} → findpeq fp } 
+
+_3⊆b_ : (f g : List Three) → Bool
+[] 3⊆b [] = true
+[] 3⊆b (j2 ∷ g) = [] 3⊆b g
+[] 3⊆b (_ ∷ g) = true
+(j2 ∷ f) 3⊆b [] = f 3⊆b []
+(j2 ∷ f) 3⊆b (_ ∷ g)  = f 3⊆b g
+(j0 ∷ f) 3⊆b (j0 ∷ g) = f 3⊆b g
+(j1 ∷ f) 3⊆b (j1 ∷ g) = f 3⊆b g
+_ 3⊆b _ = false 
+
+_3⊆_ : (f g : List Three) → Set
+f 3⊆ g  = (f 3⊆b g) ≡ true
+
+_3∩_ : (f g : List Three) → List Three
+[] 3∩ (j2 ∷ g) = j2 ∷ ([] 3∩ g)
+[] 3∩ g  = []
+(j2 ∷ f) 3∩ [] = j2 ∷ f 3∩ []
+f 3∩ [] = []
+(j0 ∷ f) 3∩ (j0 ∷ g) = j0 ∷ ( f 3∩ g )
+(j1 ∷ f) 3∩ (j1 ∷ g) = j1 ∷ ( f 3∩ g )
+(_ ∷ f) 3∩ (_ ∷ g)   = j2 ∷ ( f 3∩ g )
+
+3∩⊆f : { f g : List Three } → (f 3∩ g ) 3⊆ f
+3∩⊆f {[]} {[]} = refl
+3∩⊆f {[]} {j0 ∷ g} = refl
+3∩⊆f {[]} {j1 ∷ g} = refl
+3∩⊆f {[]} {j2 ∷ g} = 3∩⊆f {[]} {g} 
+3∩⊆f {j0 ∷ f} {[]} = refl
+3∩⊆f {j1 ∷ f} {[]} = refl
+3∩⊆f {j2 ∷ f} {[]} = 3∩⊆f {f} {[]}
+3∩⊆f {j0 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j1 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j0 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j1 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j2 ∷ f} {j0 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j2 ∷ f} {j1 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j0 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j1 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
+3∩⊆f {j2 ∷ f} {j2 ∷ g} = 3∩⊆f {f} {g}
+
+3∩sym : { f g : List Three } → (f 3∩ g ) ≡ (g 3∩ f )
+3∩sym {[]} {[]} = refl
+3∩sym {[]} {j0 ∷ g} = refl
+3∩sym {[]} {j1 ∷ g} = refl
+3∩sym {[]} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {[]} {g})
+3∩sym {j0 ∷ f} {[]} = refl
+3∩sym {j1 ∷ f} {[]} = refl
+3∩sym {j2 ∷ f} {[]} = cong (λ k → j2 ∷ k) (3∩sym {f} {[]})
+3∩sym {j0 ∷ f} {j0 ∷ g} = cong (λ k → j0 ∷ k) (3∩sym {f} {g})
+3∩sym {j0 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j0 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j1 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j1 ∷ f} {j1 ∷ g} = cong (λ k → j1 ∷ k) (3∩sym {f} {g})
+3∩sym {j1 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j2 ∷ f} {j0 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j2 ∷ f} {j1 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+3∩sym {j2 ∷ f} {j2 ∷ g} = cong (λ k → j2 ∷ k) (3∩sym {f} {g})
+
+3⊆-[] : { h : List Three } → [] 3⊆ h
+3⊆-[] {[]} = refl
+3⊆-[] {j0 ∷ h} = refl
+3⊆-[] {j1 ∷ h} = refl
+3⊆-[] {j2 ∷ h} = 3⊆-[] {h}
+
+3⊆trans : { f g h : List Three } → f 3⊆ g → g 3⊆ h → f 3⊆ h
+3⊆trans {[]} {[]} {[]} f<g g<h = refl
+3⊆trans {[]} {[]} {j0 ∷ h} f<g g<h = refl
+3⊆trans {[]} {[]} {j1 ∷ h} f<g g<h = refl
+3⊆trans {[]} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {[]} {h} refl g<h
+3⊆trans {[]} {j2 ∷ g} {[]} f<g g<h = refl
+3⊆trans {[]} {j0 ∷ g} {j0 ∷ h} f<g g<h = refl
+3⊆trans {[]} {j1 ∷ g} {j1 ∷ h} f<g g<h = refl
+3⊆trans {[]} {j2 ∷ g} {j0 ∷ h} f<g g<h = refl
+3⊆trans {[]} {j2 ∷ g} {j1 ∷ h} f<g g<h = refl
+3⊆trans {[]} {j2 ∷ g} {j2 ∷ h} f<g g<h = 3⊆trans {[]} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {[]} {[]} f<g g<h = f<g
+3⊆trans {j2 ∷ f} {[]} {j0 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
+3⊆trans {j2 ∷ f} {[]} {j1 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g (3⊆-[] {h})
+3⊆trans {j2 ∷ f} {[]} {j2 ∷ h} f<g g<h = 3⊆trans {f} {[]} {h} f<g g<h 
+3⊆trans {j0 ∷ f} {j0 ∷ g} {[]} f<g ()
+3⊆trans {j0 ∷ f} {j1 ∷ g} {[]} f<g ()
+3⊆trans {j0 ∷ f} {j2 ∷ g} {[]} () g<h
+3⊆trans {j1 ∷ f} {j0 ∷ g} {[]} f<g ()
+3⊆trans {j1 ∷ f} {j1 ∷ g} {[]} f<g ()
+3⊆trans {j1 ∷ f} {j2 ∷ g} {[]} () g<h
+3⊆trans {j2 ∷ f} {j2 ∷ g} {[]} f<g g<h = 3⊆trans {f} {g} {[]} f<g g<h 
+3⊆trans {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g g<h = 3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
+3⊆trans {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g g<h =  3⊆trans {f} {g} {h} f<g g<h 
 
-record _f⊆_ (f g : PFunc) : Set (suc n) where
+3⊆∩f : { f g h : List Three }  → f 3⊆ g → f 3⊆ h → f 3⊆  (g 3∩ h ) 
+3⊆∩f {[]} {[]} {[]} f<g f<h = refl
+3⊆∩f {[]} {[]} {x ∷ h} f<g f<h = 3⊆-[] {[] 3∩ (x ∷ h)}
+3⊆∩f {[]} {x ∷ g} {h} f<g f<h = 3⊆-[] {(x ∷ g) 3∩ h}
+3⊆∩f {j2 ∷ f} {[]} {[]} f<g f<h = 3⊆∩f {f} {[]} {[]} f<g f<h 
+3⊆∩f {j2 ∷ f} {[]} {j0 ∷ h} f<g f<h = f<g
+3⊆∩f {j2 ∷ f} {[]} {j1 ∷ h} f<g f<h = f<g
+3⊆∩f {j2 ∷ f} {[]} {j2 ∷ h} f<g f<h = 3⊆∩f {f} {[]} {h} f<g f<h 
+3⊆∩f {j0 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h = 3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j1 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j0 ∷ g} {[]} f<g f<h = f<h
+3⊆∩f {j2 ∷ f} {j0 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j0 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j0 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j1 ∷ g} {[]} f<g f<h = f<h
+3⊆∩f {j2 ∷ f} {j1 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j1 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j1 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j2 ∷ g} {[]} f<g f<h = 3⊆∩f {f} {g} {[]} f<g f<h  
+3⊆∩f {j2 ∷ f} {j2 ∷ g} {j0 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j2 ∷ g} {j1 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+3⊆∩f {j2 ∷ f} {j2 ∷ g} {j2 ∷ h} f<g f<h =  3⊆∩f {f} {g} {h} f<g f<h 
+
+↑app :(Nat → Two) → Nat → List Three  → List Three 
+↑app f Zero y = y
+↑app f (Suc x) y with f x
+... | i0 = ↑app f x (j0 ∷ y )
+... | i1 = ↑app f x (j1 ∷ y )
+
+_3↑_ : (Nat → Two) → Nat → List Three
+f 3↑ x = ↑app f x [] 
+
+listn : Nat → List Nat
+listn 0 = []
+listn (Suc n) = n ∷ listn n
+
+rev : {A : Set} → List A → List A
+rev {A} x = rev1 x [] where
+    rev1 : List A → List A → List A
+    rev1 [] y = y
+    rev1 (h ∷ x) y = rev1 x (h ∷ y)
+
+Lmap : {A B : Set} → (A → B ) → List A → List B
+Lmap f [] = []
+Lmap f (h ∷ t) = f h ∷ Lmap f t
+
+3↑1 : (Nat → Two) → Nat → List Three
+3↑1 f i with f i
+... | i0 = Lmap (λ x → j0) (rev ( listn i ))
+... | i1 = Lmap (λ x → j1) (rev ( listn i ))
+
+3↑<1 : {f : Nat → Two} → { x y : Nat } → x ≤ y → (3↑1 f x)  3⊆ (3↑1 f y)
+3↑<1 {f} {x} {y} x<y  = lemma (rev ( listn x )) where
+     lemma : (z : List Nat ) → {!!}
+     lemma = {!!}
+
+
+3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (f 3↑ x)  3⊆ (f 3↑ y)
+3↑< {f} {x} {y} x<y = {!!} where
+    lemma0 : (i : Nat) → (y : List Three ) → ( ↑app f (Suc i) y ≡ ↑app f i (j0 ∷ y)) ∨ ( ↑app f (Suc i) y ≡ ↑app f i (j1 ∷ y))
+    lemma0 i y with f i
+    lemma0 i y | i0 = case1 refl
+    lemma0 i y | i1 = case2 refl
+    lemma : (i : Nat) → (f 3↑ i)  3⊆ (f 3↑ Suc i)
+    lemma i with f i
+    lemma i | i0 = {!!}
+    lemma i | i1 = {!!}
+
+record Finite3 (p : List Three ) : Set  where
+   field
+     3-max :  Nat 
+     3-func :  Nat → Two
+     3-p⊆f :  p 3⊆ (3-func 3↑ 3-max)
+     3-f⊆p :  (3-func 3↑ 3-max) 3⊆ p 
+
+Finite3b : (p : List Three ) → Bool 
+Finite3b [] = true
+Finite3b (j0 ∷ f) = Finite3b f
+Finite3b (j1 ∷ f) = Finite3b f
+Finite3b (j2 ∷ f) = false
+
+finite3cov : (p : List Three ) → List Three
+finite3cov [] = []
+finite3cov (j0 ∷ x) = j0 ∷ finite3cov x
+finite3cov (j1 ∷ x) = j1 ∷ finite3cov x
+finite3cov (j2 ∷ x) = j0 ∷ finite3cov x
+
+Dense-3 : F-Dense (List Three) (λ x → One) _3⊆_ _3∩_
+Dense-3 = record {
+       dense =  λ x → Finite3b x ≡ true
+    ;  d⊆P = OneObj
+    ;  dense-f = λ x → finite3cov x
+    ;  dense-d = λ {p} d → lemma1 p
+    ;  dense-p = λ {p} d → lemma2 p
+  } where
+      lemma1 : (p : List Three ) → Finite3b (finite3cov p) ≡ true
+      lemma1 [] = refl
+      lemma1 (j0 ∷ p) = lemma1 p
+      lemma1 (j1 ∷ p) = lemma1 p
+      lemma1 (j2 ∷ p) = lemma1 p
+      lemma2 : (p : List Three) → p 3⊆ finite3cov p
+      lemma2 [] = refl
+      lemma2 (j0 ∷ p) = lemma2 p
+      lemma2 (j1 ∷ p) = lemma2 p
+      lemma2 (j2 ∷ p) = lemma2 p
+
+record 3Gf (f : Nat → Two) (p : List Three ) : Set where
+   field
+     3gn  : Nat
+     3f<n : (f 3↑ 3gn) 3⊆ p
+
+open 3Gf
+
+min  = Data.Nat._⊓_
+-- m≤m⊔n  = Data.Nat._⊔_
+open import Data.Nat.Properties
+
+3GF : {n : Level } → (Nat → Two ) → F-Filter (List Three) (λ x → One) _3⊆_ _3∩_
+3GF {n} f = record {  
+       filter = λ p → 3Gf f p
+     ; f⊆P = OneObj
+     ; filter1 = λ {p} {q} _ fp p⊆q → lemma1 p q fp p⊆q
+     ; filter2 = λ {p} {q} fp fq  → record { 3gn = min (3gn fp) (3gn fq) ; 3f<n = lemma2 p q fp fq }
+ }  where
+      lemma1 : (p q : List Three ) → (fp : 3Gf f p) →  (p⊆q : p 3⊆ q) → 3Gf f q
+      lemma1 p q fp p⊆q  = record { 3gn = 3gn fp  ; 3f<n = 3⊆trans {f 3↑ 3gn fp } {p} {q} (3f<n fp) p⊆q }
+      lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (f 3↑ min (3gn fp) (3gn fq)) 3⊆ (p 3∩ q)
+      lemma2 p q fp fq = 3⊆∩f {f 3↑ min (3gn fp) (3gn fq) } {p} {q} (3⊆trans {bb} {f 3↑ (3gn fp)} {p} (3↑< {_} {bm} (m⊓n≤m _ _ )) (3f<n fp))
+                                                                    (3⊆trans {bb} {f 3↑ (3gn fq)} {q} (3↑< {_} {bm} (m⊓n≤n _ _ )) (3f<n fq))  where
+             bb = f 3↑ min (3gn fp) (3gn fq)
+             bm =  min (3gn fp) (3gn fq)
+
+record _f⊆_ {n : Level } (f g : PFunc {n} ) : 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∩_ : {n : Level} → (f g : PFunc {n} ) → PFunc {n}
 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 { dom = λ x → Lift n (x ≤ i) ; map = λ x _ → f x ; meq = λ {x} {p} {q} → refl }
+_↑_ : {n : Level} → (Nat → Two) → Nat → PFunc {n}
+_↑_ {n} 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
+record Gf {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where
    field
      gn  : Nat
      f<n :  (f ↑ gn) f⊆ p
 
-record FiniteF  (p : PFunc ) : Set (suc n) where
+record FiniteF {n : Level} (p : PFunc {n} ) : Set (suc n) where
    field
      f-max :  Nat 
      f-func :  Nat → Two
@@ -261,25 +487,25 @@
 
 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 → {!!}
-  }
+-- 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 = {!!} ; map = {!!} }
+--     ;  dense-d = λ {p} d → {!!}
+--     ;  dense-p = λ {p} d → {!!}
+--   }
 
 open Gf
 
-GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
-GF f = record {  
+GF : {n : Level } → (Nat → Two ) → F-Filter (PFunc {n}) (λ x → Lift (suc n) (One {n})  ) _f⊆_ _f∩_
+GF {n} f = record {  
        filter = λ p → Gf f p
      ; f⊆P = lift OneObj
      ; filter1 = λ {p} {q} _ fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
      ; 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 : PFunc {n} } → (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  (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
@@ -289,8 +515,9 @@
             ≡⟨ 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 : PFunc {n} } → (fp : Gf {n} f p ) → (fq : Gf {n} f q ) → (f ↑ (min (gn fp) (gn fq)))  f⊆ (p f∩ q)
      f2 {p} {q} fp fq  = record { extend = λ  {x} x<g → lemma2 x<g ; feq = λ {x} {fr} → lemma3 fr } where
+            fmin : PFunc {n}
             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
@@ -391,6 +618,6 @@
 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 = {!!} }
+Hω2f→Hω2 p = {!!} -- record { od = record { def = λ x → (p {!!} ≡ i0 ) ∨ (p {!!} ≡ i1 )}; odmax = {!!} ; <odmax = {!!} }