### view filter.agda @ 292:773e03dfd6ed

...
author Shinji KONO Sat, 13 Jun 2020 15:59:10 +0900 ef93c56ad311 9972bd4a0d6f
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⊔_ )

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom

open _∧_
open _∨_
open Bool

_∩_ : ( A B : OD  ) → OD
A ∩ B = record { def = λ x → def A x ∧ def B x }

_∪_ : ( A B : OD  ) → OD
A ∪ B = record { def = λ x → def A x ∨ def B x }

_＼_ : ( A B : OD  ) → OD
A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }

-- Kunen p.76 and p.53
record Filter  ( L : OD  ) : Set (suc n) where
field
filter : OD
f⊆PL :  filter ⊆ Power L
filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)

open Filter

proper-filter : {L : OD} → (P : Filter L ) → {p : OD} → Set n
proper-filter {L} P {p} = filter P ∋ L

prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )

record Ideal  ( L : OD  ) : Set (suc n) where
field
ideal : OD
i⊆PL :  ideal ⊆ Power L
ideal1 : { p q : OD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
ideal2 : { p q : OD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)

open Ideal

proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
proper-ideal {L} P {p} = ideal P ∋ od∅

prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )

ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set n
ultra-filter {L} P {p} = L ∋ p →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )

filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
filter-lemma1 {L} P {p} {q} u lt = {!!}

filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p}
filter-lemma2 {L} P prime p with prime {!!}
... | t = {!!}

generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
generated-filter {L} P p = record {
filter = {!!}  ;
filter1 = {!!} ; filter2 = {!!}
}

record Dense  (P : OD ) : Set (suc n) where
field
dense : OD
incl :  dense ⊆ P
dense-f : OD → OD
dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p)

-- H(ω,2) = Power ( Power ω ) = Def ( Def ω))

infinite = ZF.infinite OD→ZF

module in-countable-ordinal {n : Level} where

import ordinal

-- open  ordinal.C-Ordinal-with-choice

Hω2 : Filter (Power (Power infinite))
Hω2 = {!!}

```