open import Level
open import Ordinals
module filter {n : Level } (O : Ordinals {n})   where

open import zf
open import logic
import OD 

open import Relation.Nullary 
open import Relation.Binary 
open import Data.Empty 
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
import BAlgbra 

open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

import ODC

open _∧_
open _∨_
open Bool

-- Kunen p.76 and p.53, we use ⊆
record Filter  ( L : HOD  ) : Set (suc n) where
   field
       filter : HOD   
       f⊆PL :  filter ⊆ Power L 
       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

open Filter

record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter P ∋ od∅)
       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
   field
       proper  : ¬ (filter P ∋ od∅)
       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )

open _⊆_

trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }

refl-⊆ : {A : HOD} → A ⊆ A
refl-⊆ {A} = record { incl = λ x → x }

power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
   t1 = zf.IsZF.power→ isZF A t PA∋t

∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )

∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }

∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }

q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
q∩q⊆q = record { incl = λ lt → proj1 lt } 

open HOD

-----
--
--  ultra filter is prime
--

filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P 
filter-lemma1 {L} P u = record {
         proper = ultra-filter.proper u
       ; prime = lemma3
    } where
  lemma3 : {p q : HOD} → 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)) =h=  (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 }
      } where
         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
         lemma4 x lt with proj1 lt
         lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
         lemma4 x lt | case2 qx = qx
    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
    lemma6 = filter2 P lt ¬p∈P
    lemma7 : filter P ∋ (q ∩ (L ＼ p))
    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
    lemma8 : (q ∩ (L ＼ p)) ⊆ q
    lemma8 = q∩q⊆q

-----
--
--  if Filter contains L, prime filter is ultra
--

filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
filter-lemma2 {L} P f∋L prime = record {
         proper = prime-filter.proper prime
       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
   } where
        open _==_
        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
        eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x  )) 
        eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
        lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L

record Dense  (P : HOD ) : Set (suc n) where
   field
       dense : HOD
       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) 

record Ideal  ( L : HOD  ) : Set (suc n) where
   field
       ideal : HOD   
       i⊆PL :  ideal ⊆ Power L 
       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

open Ideal

proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
proper-ideal {L} P {p} = ideal P ∋ od∅

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 )

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
       f⊆P :  PL filter 
       filter1 : { p q : L } → PL (λ x → q ⊆ x )  → filter p →  p ⊆ q  → filter q
       filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)

Filter-is-F : {L : HOD} → (f : Filter L ) → F-Filter HOD (λ p → (x : HOD) → p x → x ⊆ L ) _⊆_ _∩_
Filter-is-F {L} f = record {
       filter = λ x → Lift (suc n) ((filter f) ∋ x)
     ; f⊆P = λ x f∋x →  power→⊆ _ _ (incl ( f⊆PL f  ) (lower f∋x ))
     ; filter1 = λ {p} {q} q⊆L f∋p  p⊆q → lift ( filter1 f (q⊆L q refl-⊆) (lower f∋p) p⊆q)
     ; 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 where
   i0 : Two
   i1 : Two

data Three : Set where
   j0 : Three
   j1 : Three
   j2 : Three

open import Data.List hiding (map)

import OPair
open OPair O

record PFunc {n : Level} : 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 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) 

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 

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 

3↑22 : (f : Nat → Two) (i j : Nat) → List Three
3↑22 f Zero j = []
3↑22 f (Suc i) j with f j
3↑22 f (Suc i) j | i0 = j0 ∷ 3↑22 f i (Suc j)
3↑22 f (Suc i) j | i1 = j1 ∷ 3↑22 f i (Suc j)

_3↑_ : (Nat → Two) → Nat → List Three
_3↑_ f i = 3↑22 f i 0 

3↑< : {f : Nat → Two} → { x y : Nat } → x ≤ y → (_3↑_ f x)  3⊆ (_3↑_ f y)
3↑< {f} {x} {y} x<y = lemma x y 0 x<y where
     lemma : (x y i : Nat) → x ≤ y → (3↑22 f x i ) 3⊆ (3↑22 f y i )
     lemma 0 y i z≤n with f i
     lemma Zero Zero i z≤n | i0 = refl
     lemma Zero (Suc y) i z≤n | i0 = 3⊆-[]  {3↑22 f (Suc y) i}
     lemma Zero Zero i z≤n | i1 = refl
     lemma Zero (Suc y) i z≤n | i1 = 3⊆-[]  {3↑22 f (Suc y) i}
     lemma (Suc x) (Suc y) i (s≤s x<y) with f i  
     lemma (Suc x) (Suc y) i (s≤s x<y) | i0 = lemma x y (Suc i) x<y 
     lemma (Suc x) (Suc y) i (s≤s x<y) | i1 = lemma x y (Suc i) x<y 

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 : p 3⊆ (f 3↑ 3gn)

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 = {!!} }
      lemma2 : (p q : List Three ) → (fp : 3Gf f p) → (fq : 3Gf f q)  → (p 3∩ q) 3⊆ (f 3↑ min (3gn fp) (3gn fq))
      lemma2 p q fp 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⊆_

_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 }

_↑_ : {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 {n : Level} (f : Nat → Two) (p : PFunc {n} ) : Set (suc n) where
   field
     gn  : Nat
     f<n :  (f ↑ gn) f⊆ p

record FiniteF {n : Level} (p : PFunc {n} ) : 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 = {!!} ; map = {!!} }
--     ;  dense-d = λ {p} d → {!!}
--     ;  dense-p = λ {p} d → {!!}
--   }

open Gf

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 {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
             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 {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
                   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)) 

data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
  hφ :  Hω2 0 o∅
  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 0 >) ,  ord→od x )))
  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) (od→ord (Union ((< nat→ω i , nat→ω 1 >) ,  ord→od x )))
  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) x

record  Hω2r (x : Ordinal) : Set n where
  field
    count : Nat
    hω2 : Hω2 count x

open Hω2r

HODω2 :  HOD
HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
    ω<next = ω<next-o∅ ho<
    lemma : {i j : Nat} {x : Ordinal } → od→ord (Union (< nat→ω i , nat→ω j > , ord→od x)) o< next x
    lemma = {!!}
    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
    odmax0 {y} r with hω2 r
    ... | hφ = x<nx
    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {0} {x})
    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma {i} {1} {x})
    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx

3→Hω2 : List Three → HOD
3→Hω2 t = list→hod t 0 where
   list→hod : List Three → Nat → HOD
   list→hod [] _ = od∅
   list→hod (j0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
   list→hod (j1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
   list→hod (j2 ∷ t) i = list→hod t (Suc i ) 

Hω2→3 : (x :  HOD) → HODω2 ∋ x → List Three 
Hω2→3 x = lemma where
   lemma : { y : Ordinal } →  Hω2r y → List Three
   lemma record { count = 0 ; hω2 = hφ } = []
   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = j0 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = j1 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (he hω3) } = j2 ∷ lemma record { count = i ; hω2 =  hω3 }

ω→2 : HOD
ω→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
  ... | no _  = nat→ω 0

ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
ω→2f x = {!!}

↑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) ))

record Gfo (x : Ordinal) : Set n where
  field
     gfunc : Ordinal
     gmax : Ordinal
     gcond : (odef ω→2  gfunc) ∧ (odef infinite gmax)
     gfdef : {!!} -- ( ↑n (ord→od gfunc) (ord→od gmax) (subst₂ ? ? ? gcond) )  ⊆ ord→od x 
     pcond : odef HODω2 x

open Gfo

HODGf : HOD
HODGf = record { od = record { def = λ x → Gfo x } ; odmax = next o∅ ; <odmax = {!!} }

G : (Nat → Two) → Filter HODω2
G f = record {
       filter = HODGf
     ; f⊆PL = {!!}
     ; filter1 = {!!}
     ; filter2 = {!!}
   } where
       filter0 : HOD   
       filter0 = {!!}
       f⊆PL1 :  filter0 ⊆ Power HODω2 
       f⊆PL1 = {!!}
       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
       filter11 = {!!}
       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
       filter12 = {!!}

-- 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
       ctl→ : Nat → Ordinal
       ctl← : Ordinal → Nat
       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x 
       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
       
record GenericFilter (P : HOD) : Set (suc n) where
    field
       genf : Filter P
       generic : (D : Dense P ) → ¬ ( (Dense.dense D ∩ Filter.filter genf ) ≡ od∅ )

record F-GenericFilter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
       GFilter : F-Filter L PL _⊆_ _∩_
       Intersection : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → F-Dense.dense D x →  L
       Generic : (D : F-Dense L PL _⊆_ _∩_ ) → { x : L } → ( y : F-Dense.dense D x) →  F-Filter.filter GFilter (Intersection D y )

data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (n : Nat) →  Set (suc n) where
    pd0 : (p : Ordinal ) → odef (ord→od P) p → PD C p 0 
    pdq : {q pnx : Ordinal } {n : Nat}  → (pn : PD P C pnx n ) → odef (ctl→ C n) q → ord→od p0x ⊆ ord→od q → PD P C q (suc n) 

P-GenericFilter : {P : HOD} → (C : CountableOrdinal) → GenericFilter P
P-GenericFilter {P} C = record {
      genf = record { filter = {!!} ; f⊆PL = {!!} ; filter1 = {!!} ; filter2 = {!!} }
    ; generic = λ D → {!!}
   }