Mercurial > hg > Members > kono > Proof > ZF-in-agda
view filter.agda @ 384:171a3d587d6e
Three List / Filter
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 22 Jul 2020 00:20:33 +0900 |
parents | 5994f10d9bfd |
children | 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 = {!!} }