--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/generic-filter.agda	Sat Jul 25 09:09:00 2020 +0900
@@ -0,0 +1,269 @@
+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 Gf (f : Nat → Two) (p :  PFunc (Lift n Nat) (Lift n Two) ) : Set (suc n) where
+   field
+     gn  : Nat
+     f<n :  (f ↑ gn) f⊆ p
+
+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 Gf
+open _f⊆_ 
+open import Data.Nat.Properties
+
+GF :  (Nat → Two ) → F-Filter (PFunc (Lift n Nat) (Lift n Two)) (λ x → Lift (suc n) (One {n})  ) _f⊆_ _f∩_
+GF  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 (Lift n Nat) (Lift n Two) } → (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)} → pmap (f ↑ gn fp) (lift x) fr ≡ pmap q (lift x) (extend p⊆q (extend (f<n fp) fr))
+         lemma {x} {fr} = begin
+             pmap (f ↑ gn fp) (lift x) fr
+            ≡⟨ feq (f<n fp )  ⟩
+             pmap p (lift x) (extend (f<n fp)  fr)
+            ≡⟨ feq p⊆q  ⟩
+             pmap q (lift x) (extend p⊆q  (extend (f<n fp)  fr))
+            ∎  where open ≡-Reasoning 
+     f2 : {p q : PFunc (Lift n Nat) (Lift n Two) } → (fp : Gf  f p ) → (fq : Gf  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 (Lift n Nat) (Lift n Two)
+            fmin =  f ↑  (min (gn fp) (gn fq)) 
+            lemma1 : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → (fr : dom p (lift x)) (gr : dom q (lift x)) → pmap p (lift x) fr ≡ pmap q (lift x) gr
+            lemma1 {x} x<g fr gr = begin
+                   pmap p (lift x) fr 
+                ≡⟨ meq p ⟩
+                   pmap p (lift x) (extend (f<n fp) (lift ( ≤-trans (lower x<g) (m⊓n≤m _ _))))
+                ≡⟨ sym (feq (f<n fp)) ⟩
+                   pmap (f ↑  (min (gn fp) (gn fq))) (lift x) x<g
+                ≡⟨ feq (f<n fq) ⟩
+                   pmap q (lift x) (extend (f<n fq) (lift ( ≤-trans (lower x<g) (m⊓n≤n _ _))))
+                ≡⟨ meq q ⟩
+                   pmap q (lift x) gr
+                ∎  where open ≡-Reasoning 
+            lemma2  : {x : Nat}  → ( x<g : Lift n (x ≤ min (gn fp) (gn fq)) ) → dom (p f∩ q) (lift 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 (Lift n Nat) (Lift n Two) ) → (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)))  → pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr ≡ pmap (p f∩ q) (lift x) (lemma2 fr)
+            lemma3 {x} fr = 
+                  pmap (f ↑ min (gn fp) (gn fq)) (lift x) fr
+                ≡⟨ feq (f<n fq) ⟩
+                  pmap q (lift x) (extend (f<n fq) ( lift (≤-trans (lower fr) (m⊓n≤n _ _)) ))
+                ≡⟨ sym (feq (f∩→⊆ p q ) {x} {lemma2 fr} )   ⟩
+                  pmap (p f∩ q) (lift 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 (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) ))
+
+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
+       
+open CountableOrdinal 
+
+PGOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Set n
+PGOD  i C p q =  ¬ ( odef (ord→od (ctl→ C i)) q ∧ ( (x : Ordinal ) → odef (ord→od p) x →  odef (ord→od q) x ))
+
+PGHOD : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → HOD
+PGHOD i C p = record { od = record { def = λ x → PGOD i C {!!} {!!} } ; odmax = {!!} ; <odmax = {!!} } 
+
+ord-compare : (i : Nat) → (C : CountableOrdinal) → (p : Ordinal) → ( q : Ordinal ) → Ordinal
+ord-compare i C p q with ODC.p∨¬p O ( (q : Ordinal ) → PGOD i C p q )
+ord-compare i C p q | case1 y = p
+ord-compare i C p q | case2 n = od→ord (ODC.minimal O (PGHOD i C p ) (∅< (subst₂ (λ j k → odef j {!!} ) refl {!!} n)) ) 
+
+data PD (P : HOD) (C : CountableOrdinal) : (x : Ordinal) (i : Nat) →  Set (suc n) where
+    pd0 : PD P C o∅ 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 → {!!}
+   }