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 OrdUtil import ODUtil open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal open Ordinals.IsNext isNext open OrdUtil O open ODUtil O import ODC open filter O open _∧_ open _∨_ open Bool open HOD ------- -- the set of finite partial functions from ω to 2 -- -- open import Data.List hiding (filter) open import Data.Maybe import OPair open OPair O record CountableModel (P : HOD) : Set (suc (suc n)) where field ctl-M : Ordinal ctl→ : Nat → Ordinal ctl← : (x : Ordinal )→ x o< ctl-M → Nat is-Model : (x : Nat) → ctl→ x o< ctl-M ctl-iso→ : { x : Ordinal } → (lt : x o< ctl-M) → ctl→ (ctl← x lt ) ≡ x ctl-iso← : { x : Nat } → ctl← (ctl→ x ) (is-Model x) ≡ x ctl-P⊆M : Power P ⊆ * ctl-M -- we expect ¬ G ∈ * ctl-M, so ¬ P ∈ * ctl-M open CountableModel ---- -- a(n) ∈ M -- ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q -- PGHOD : (i : Nat) (P : HOD) (C : CountableModel P) → (p : Ordinal) → HOD PGHOD i P C p = record { od = record { def = λ x → odef (Power P) x ∧ odef (* (ctl→ C i)) x ∧ ( (y : Ordinal ) → odef (* p) y → odef (* x) y ) } ; odmax = odmax (Power P) ; } -- record valR (x y P : HOD) (G : GenericFilter P) : Set (suc n) where field p : HOD p∈G : filter (genf G) ∋ p is-val : x ∋ < y , p > val : (x : HOD) (P : HOD ) → (G : GenericFilter P) → HOD val x P G = record { od = record { odef = ε-induction { λ y → (z : Ordinal) → odef y (& z) → {!!} } (λ {z} Prev → {!!} ) } ; odmax = {!!} ;