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

diff -r e75402b1f7d4 -r 8c3b59f583f2 filter.agda
--- a/filter.agda	Sun Jul 19 16:19:24 2020 +0900
+++ b/filter.agda	Sun Jul 19 19:14:12 2020 +0900
@@ -168,26 +168,22 @@
      extend : (x : Nat) → (fr : restrict f x ) →  restrict g x  
      feq : (x : Nat) → (fr : restrict f x ) →  map f x fr ≡ map g x (extend x fr)
 
-record  _f∩_ (f g : PFunc) : Set (suc n) where
-  field
-     pf : PFunc
-     f< : f f⊆ pf
-     g< : g f⊆ pf
+open _f⊆_
 
-full-func  : Set n
-full-func = Nat → Two
-
-full→PF : (Nat → Two) → PFunc
-full→PF f = record { restrict = λ x → One ; map = λ x _ → f x }
+_f∩_ : (f g : PFunc) → PFunc
+f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
+              ; map = λ x p →  map f x (proj1 p) }
 
 _↑_ : (Nat → Two) → Nat → PFunc
 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
 
-record gf-filter (f : Nat → Two) (p : PFunc ) : Set (suc n) where
+record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
    field
      gn  : Nat
      f<n :  p f⊆ (f ↑ gn)
 
+open Gf
+
 record F-Filter (L : Set (suc n)) (PL : (L → Set (suc n)) → Set n) ( _⊆_ : L  → L → Set (suc n))  (_∩_ : L → L → L ) : Set (suc (suc n)) where
    field
        filter : L → Set (suc n)
@@ -195,13 +191,17 @@
        filter1 : { p q : L } → filter p →  p ⊆ q  → filter q
        filter2 : { p q : L } → filter p →  filter q  → filter (p ∩ q)
 
-GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ {!!}
+GF : (Nat → Two ) → F-Filter PFunc (λ x → One) _f⊆_ _f∩_
 GF f = record {  
-       filter = λ p → gf-filter f p
+       filter = λ p → Gf f p
      ; f⊆P = OneObj
-     ; filter1 = λ {p} {q} fp p⊆q → record { gn = {!!} ; f<n = {!!} }
+     ; 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 = {!!} }
- }
+ } 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  ?
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
@@ -247,8 +247,8 @@
       -- n : HOD
       -- ? : Select f (λ x f∋x → ω→nat (π1 f∋x) < ω→nat n
   
-Gf : {f : HOD} → ω→2 ∋ f  → HOD
-Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )
+-- Gf : {f : HOD} → ω→2 ∋ f  → HOD
+-- Gf {f} lt = Select HODω2 (λ x H∋x → {!!}   )
 
 G : (Nat → Two) → Filter HODω2
 G f = record {