Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison filter.agda @ 191:9eb6a8691f02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
choice function cannot jump between ordinal level
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jul 2019 14:07:08 +0900
parents 6e778b0a7202
children 0b9645a65542
comparison
equal deleted inserted replaced
190:6e778b0a7202 191:9eb6a8691f02
8 open import Relation.Binary 8 open import Relation.Binary
9 open import Data.Empty 9 open import Data.Empty
10 open import Relation.Binary 10 open import Relation.Binary
11 open import Relation.Binary.Core 11 open import Relation.Binary.Core
12 open import Relation.Binary.PropositionalEquality 12 open import Relation.Binary.PropositionalEquality
13 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14
13 15
14 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where 16 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where
15 field 17 field
16 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) 18 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
17 G : OD {suc n} 19 G : OD {suc n}
22 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r ))) 24 ( r : OD {suc n}) → (( p ⊇ r ) ∧ ( p ⊇ r )))
23 25
24 dense : {n : Level} → Set (suc (suc n)) 26 dense : {n : Level} → Set (suc (suc n))
25 dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q )) 27 dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
26 28
29 record NatFilter {n : Level} ( P : Nat → Set n) : Set (suc n) where
30 field
31 GN : Nat → Set n
32 GN∋1 : GN 0
33 GNmax : { p : Nat } → P p → 0 ≤ p
34 GNless : { p q : Nat } → GN p → P q → q ≤ p → GN q
35 Gr : ( p q : Nat ) → GN p → GN q → Nat
36 GNcompat : { p q : Nat } → (gp : GN p) → (gq : GN q ) → ( Gr p q gp gq ≤ p ) ∨ ( Gr p q gp gq ≤ q )
37
38 record NatDense {n : Level} ( P : Nat → Set n) : Set (suc n) where
39 field
40 Gmid : { p : Nat } → P p → Nat
41 GDense : { D : Nat → Set n } → {x p : Nat } → (pp : P p ) → D (Gmid {p} pp) → Gmid pp ≤ p
42
27 open OD.OD 43 open OD.OD
28 44
29 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω)) 45 -- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
30 46
31 Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n} 47 Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
34 } 50 }
35 51
36 Hω2 : {n : Level} → OD {suc n} 52 Hω2 : {n : Level} → OD {suc n}
37 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) } 53 Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
38 54
39 _⊆_ : {n : Level} → ( A B : OD {suc n} ) → ∀{ x : OD {suc n} } → Set (suc n)
40 _⊆_ A B {x} = A ∋ x → B ∋ x
41
42 Hω2Filter : {n : Level} → Filter {n} Hω2 od∅ 55 Hω2Filter : {n : Level} → Filter {n} Hω2 od∅
43 Hω2Filter {n} = record { 56 Hω2Filter {n} = record {
44 _⊇_ = {!!} 57 _⊇_ = _⊇_
45 ; G = {!!} 58 ; G = {!!}
46 ; G∋1 = {!!} 59 ; G∋1 = {!!}
47 ; Gmax = {!!} 60 ; Gmax = {!!}
48 ; Gless = {!!} 61 ; Gless = {!!}
49 ; Gcompat = {!!} 62 ; Gcompat = {!!}