Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison filter.agda @ 287:5de8905a5a2b
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 07 Jun 2020 20:29:12 +0900 |
parents | d9d3654baee1 |
children | ef93c56ad311 |
comparison
equal
deleted
inserted
replaced
286:4ae48eed654a | 287:5de8905a5a2b |
---|---|
41 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q | 41 filter1 : { p q : OD } → q ⊆ L → filter ∋ p → p ⊆ q → filter ∋ q |
42 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) | 42 filter2 : { p q : OD } → filter ∋ p → filter ∋ q → filter ∋ (p ∩ q) |
43 | 43 |
44 open Filter | 44 open Filter |
45 | 45 |
46 L⊆L : (L : OD) → L ⊆ L | |
47 L⊆L L = record { incl = λ {x} lt → lt } | |
48 | |
46 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L | 49 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L |
47 L-filter {L} P {p} lt = filter1 P {p} {L} {!!} lt {!!} | 50 L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!} |
48 | 51 |
49 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n | 52 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n |
50 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) | 53 prime-filter {L} P {p} {q} = filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q ) |
51 | 54 |
52 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n | 55 ultra-filter : {L : OD} → Filter L → ∀ {p : OD } → Set n |
81 module in-countable-ordinal {n : Level} where | 84 module in-countable-ordinal {n : Level} where |
82 | 85 |
83 import ordinal | 86 import ordinal |
84 | 87 |
85 -- open ordinal.C-Ordinal-with-choice | 88 -- open ordinal.C-Ordinal-with-choice |
86 | 89 -- both Power and infinite is too ZF, it is better to use simpler one |
87 Hω2 : Filter (Power (Power infinite)) | 90 Hω2 : Filter (Power (Power infinite)) |
88 Hω2 = {!!} | 91 Hω2 = {!!} |
89 | 92 |