# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595156279 -32400
# Node ID b4a247f9d94084efb6a8d2b5564446d952233bc4
# Parent  8c3b59f583f278a2775d4e8079d6995dd5b83dea
...

diff -r 8c3b59f583f2 -r b4a247f9d940 filter.agda
--- a/filter.agda	Sun Jul 19 19:14:12 2020 +0900
+++ b/filter.agda	Sun Jul 19 19:57:59 2020 +0900
@@ -196,12 +196,12 @@
        filter = λ p → Gf f p
      ; f⊆P = OneObj
      ; filter1 = λ {p} {q} fp p⊆q → record { gn = gn fp ; f<n = f1 fp p⊆q }
-     ; filter2 = λ {p} {q} fp fq  → record { gn = {!!} ; f<n = {!!} }
+     ; filter2 = λ {p} {q} fp fq  → record { gn = gn fp ; f<n = f2 fp fq }
  } where
      f1 : {p q : PFunc } → (fp : Gf f p ) → ( p⊆q : p f⊆ q ) → q f⊆ (f ↑ gn fp)
-     f1 {p} {q} fp p⊆q = record { extend = λ x fr → extend (f<n fp) x {!!}  ; feq = λ x fr → {!!} } where
-         f2 : (x : Nat) →  x ≤ gn fp
-         f2 x = ? -- extend (f<n fp) x  ?
+     f1 {p} {q} fp p⊆q = record { extend = λ x fq → {!!}  ; feq = λ x fr → {!!} } where
+     f2 : {p q : PFunc } → (fp : Gf f p ) → (fq : Gf f q ) → (p f∩ q) f⊆ (f ↑ gn fp)
+     f2 {p} {q} fp fq  = record { extend = λ  x y → extend (f<n fp) x (proj1 y) ; feq = λ x fr → {!!} } where
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y))