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

import filter 
open import zf
open import logic
open import partfunc {n} O
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 filter O

open _∧_
open _∨_
open Bool


open HOD

-------
--    the set of finite partial functions from ω to 2
--
--

open import Data.List 
open import Data.Maybe 

import OPair
open OPair O

open PFunc

_f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) →  PFunc (Lift n Nat) (Lift n Two)
f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → pmap f x fr ≡ pmap g x gr)
              ; pmap = λ x p →  pmap f x (proj1  p) ; meq = meq f }

_↑_ :  (Nat → Two) → Nat →  PFunc (Lift n Nat) (Lift n Two)
_↑_  f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl }

record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two)  ) : Set (suc n) where
  field
     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)) 

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 (Maybe Two) → HOD
3→Hω2 t = list→hod t 0 where
   list→hod : List (Maybe Two) → Nat → HOD
   list→hod [] _ = od∅
   list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) )) 
   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) )) 
   list→hod (nothing ∷ t) i = list→hod t (Suc i ) 

Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two) 
Hω2→3 x = lemma where
   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
   lemma record { count = 0 ; hω2 = hφ } = []
   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ 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) ))

-- 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 CountableHOD : Set (suc (suc n)) where
   field
       phod : HOD
       ptl→ : Nat → Ordinal
       ptl→∈P : (i : Nat) → odef phod (ptl→ i)
       ptl← : (x : Ordinal) → odef phod x → Nat
       ptl-iso→ : { x : Ordinal } → (lt : odef phod x ) → ptl→ (ptl← x lt ) ≡ x 
       ptl-iso← : { x : Nat }  → ptl← (ptl→ x ) (ptl→∈P x) ≡ x
   
       
open CountableOrdinal 
open CountableHOD

PGHOD :  (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
PGHOD i C p = record { od = record { def = λ x → odef (ord→od (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (ord→od p) y →  odef (ord→od x) y ) }
   ; odmax = ctl→ C i  ; <odmax = λ {y} lt → odefo→o< (proj1 lt)}  

next-p : (P : CountableHOD ) (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → Ordinal
next-p P i C p with ODC.decp O ( PGHOD i C p =h= od∅ )
next-p P i C p | yes y = p
next-p P i C p | no not = od→ord (ODC.minimal O (PGHOD i C p ) not)

data PD (P : CountableHOD ) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set n where
    pd0 : PD P C o∅ 0 
    pdsuc : {p : Ordinal } {i : Nat} → PD P C p i  → PD P C (next-p P i C p) (Suc i) 

record PDN (P : CountableHOD ) (C : CountableOrdinal) (x : Ordinal) : Set n where
   field
       px∈ω : odef (phod P) x
       pdod : PD P C x (ptl← P x px∈ω)

open PDN

PDHOD : (P : CountableHOD ) → (C : CountableOrdinal) → HOD
PDHOD P C = record { od = record { def = λ x →  PDN P C x }
    ; odmax = odmax (phod P) ; <odmax = λ {y} lt → <odmax (phod P) (px∈ω lt) } where

--
--  p 0 ≡ ∅
--  p (suc n) = if ∃ q ∈ ord→od ( ctl→ n ) ∧ p n ⊆ q → q 
---             else p n

ψ : HOD  → Set n
ψ y = (lt : odef infinite (od→ord y) ) →  Hω2 (ω→nat y lt ) (od→ord y )
ind : (C : CountableOrdinal) → {x : HOD} → ({y : HOD} → OD.def (od x) (od→ord y) →
   (lt : infinite-d (od→ord y)) → Hω2 (ω→nat y lt) (od→ord y)) →
   (lt : infinite-d (od→ord x)) → Hω2 (ω→nat x lt) (od→ord x)
ind C {x} prev lt with ω→nat x lt
... | Zero = subst (λ k → Hω2 Zero k) {!!} hφ
... | Suc i with ODC.decp O ( PGHOD i C {!!} =h= od∅ ) | prev {{!!}} {!!} {!!}
ind C {x} prev lt | Suc i | yes p | s1 = he ?
ind C {x} prev lt | Suc i | no ¬p | s1 = {!!}

Gω2r :  (C : CountableOrdinal) → (x : Ordinal) → (lt : infinite ∋ ord→od x ) →  Hω2 (ω→nat (ord→od x) lt ) x
Gω2r C x = subst (λ k → (lt : odef infinite (od→ord (ord→od x))) →  Hω2 (ω→nat (ord→od x) lt ) k ) diso ( ε-induction {ψ} (ind C) (ord→od x)) 

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