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