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

diff -r 1425104bb5d8 -r e75402b1f7d4 filter.agda
--- a/filter.agda	Sun Jul 19 12:26:17 2020 +0900
+++ b/filter.agda	Sun Jul 19 16:19:24 2020 +0900
@@ -165,7 +165,14 @@
 
 record _f⊆_ (f g : PFunc) : Set (suc n) where
   field
-     feq : (x : Nat) → (fr : restrict f x ) →  (gr : restrict g x ) → map f x fr ≡ map g x gr
+     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
 
 full-func  : Set n
 full-func = Nat → Two
@@ -176,12 +183,25 @@
 _↑_ : (Nat → Two) → Nat → PFunc
 f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
 
-record F-Filter (PL : Set n) (L : PL ) ( _⊆_ : PL → PL → Set n) ( _∋_ : PL → PL → Set n) : Set (suc n) where
+record gf-filter (f : Nat → Two) (p : PFunc ) : Set (suc n) where
+   field
+     gn  : Nat
+     f<n :  p f⊆ (f ↑ gn)
+
+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 : PL
-       f⊆PL :  filter ⊆ L
-       filter1 : { p q : PL } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
-       filter2 : { p q : PL } → filter ∋ p →  filter ∋ q  → (filter ∋ p) ∧ (filter ∋ q)
+       filter : L → Set (suc n)
+       f⊆P :  PL filter 
+       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 f = record {  
+       filter = λ p → gf-filter f p
+     ; f⊆P = OneObj
+     ; filter1 = λ {p} {q} fp p⊆q → record { gn = {!!} ; f<n = {!!} }
+     ; filter2 = λ {p} {q} fp fq  → record { gn = {!!} ; f<n = {!!} }
+ }
 
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y))