# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1569846127 -32400
# Node ID 7b4a66710cdd41aef8351dc1891f2631e058ad3c
# Parent  e469de3ae7ccef913dda22a39be8c47b076f4a69
...

diff -r e469de3ae7cc -r 7b4a66710cdd filter.agda
--- 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 = {!!} }