### view filter.agda @ 384:171a3d587d6e

Three List / Filter
author Shinji KONO Wed, 22 Jul 2020 00:20:33 +0900 5994f10d9bfd edbf7459a85f
line wrap: on
line source
```
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

lemma12 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j0 ∷ t))
lemma12 s t eq = eq
lemma13 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j1 ∷ t))
lemma13 s t eq = eq
lemma14 : (s t : List Three ) → (s 3⊆ t) → ((j2 ∷ s) 3⊆ (j2 ∷ t))
lemma14 s t eq = eq

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

_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

ω→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

record _↑n (f : HOD) (ω→2∋f : ω→2 ∋ f ) : Set n where
-- field
-- n : HOD
-- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n

-- Gf : {f : HOD} → ω→2 ∋ f  → HOD
-- Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )

G : (Nat → Two) → Filter HODω2
G f = record {
filter = {!!}
; 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 = {!!} }

```