Mercurial > hg > Members > kono > Proof > ZF-in-agda
view filter.agda @ 246:3506f53c7d83
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Aug 2019 02:50:16 +0900 |
parents | 650bdad56729 |
children | 9bf100ae50ac |
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 _∧_ open _∨_ open Bool record Filter ( P max : OD ) : Set (suc n) where field _⊇_ : OD → OD → Set n G : OD G∋1 : G ∋ max Gmax : { p : OD } → P ∋ p → p ⊇ max Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) dense : Set (suc n) dense = { D P p : OD } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q )) record NatFilter ( P : Nat → Set n) : Set (suc n) where field GN : Nat → Set n GN∋1 : GN 0 GNmax : { p : Nat } → P p → 0 ≤ p GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q Gr : ( p q : Nat ) → GN p → GN q → Nat GNcompat : { p q : Nat } → (gp : GN p) → (gq : GN q ) → ( Gr p q gp gq ≤ p ) ∨ ( Gr p q gp gq ≤ q ) record NatDense {n : Level} ( P : Nat → Set n) : Set (suc n) where field Gmid : { p : Nat } → P p → Nat GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) → Gmid pp ≤ p open OD.OD -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) Pred : ( Dom : OD ) → OD Pred dom = record { def = λ x → def dom x → {!!} } Hω2 : OD Hω2 = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) } Hω2Filter : Filter Hω2 od∅ Hω2Filter = record { _⊇_ = _⊇_ ; G = {!!} ; G∋1 = {!!} ; Gmax = {!!} ; Gless = {!!} ; Gcompat = {!!} } where P = Hω2 _⊇_ : OD → OD → Set n _⊇_ = {!!} G : OD G = {!!} G∋1 : G ∋ od∅ G∋1 = {!!} Gmax : { p : OD } → P ∋ p → p ⊇ od∅ Gmax = {!!} Gless : { p q : OD } → G ∋ p → P ∋ q → p ⊇ q → G ∋ q Gless = {!!} Gcompat : { p q : OD } → G ∋ p → G ∋ q → ¬ ( ( r : OD ) → (( p ⊇ r ) ∧ ( p ⊇ r ))) Gcompat = {!!}