Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 268:7b4a66710cdd
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Sep 2019 21:22:07 +0900 |
| parents | e469de3ae7cc |
| children | 30e419a2be24 |
| files | filter.agda |
| diffstat | 1 files changed, 5 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/filter.agda Mon Sep 30 20:59:45 2019 +0900 +++ b/filter.agda Mon Sep 30 21:22:07 2019 +0900 @@ -30,7 +30,7 @@ record Filter ( L : OD ) : Set (suc n) where field - F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ p q {x} ) → L ∋ q + F1 : { p q : OD } → L ∋ p → ({ x : OD} → _⊆_ q p {x} ) → L ∋ q F2 : { p q : OD } → L ∋ p → L ∋ q → L ∋ (p ∩ q) open Filter @@ -52,7 +52,9 @@ filter-lemma1 {L} P {p} {q} u lt | case1 x | case1 y = case1 x filter-lemma1 {L} P {p} {q} u lt | case1 x | case2 y = case1 x filter-lemma1 {L} P {p} {q} u lt | case2 x | case1 y = case2 y -filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim ( y ? ) +filter-lemma1 {L} P {p} {q} u lt | case2 x | case2 y = ⊥-elim (lemma (record { proj1 = x ; proj2 = y })) where + lemma : ¬ ( ¬ ( L ∋ p ) ) ∧ ( ¬ ( L ∋ q )) + lemma = {!!} 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 { @@ -64,5 +66,5 @@ infinite = ZF.infinite OD→ZF Hω2 : Filter (Power (Power infinite)) -Hω2 = {!!} +Hω2 = record { F1 = {!!} ; F2 = {!!} }