### changeset 268:7b4a66710cdd

...
author Shinji KONO Mon, 30 Sep 2019 21:22:07 +0900 e469de3ae7cc 30e419a2be24 filter.agda 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 = {!!} }
```