--- a/filter.agda	Mon Jul 20 12:17:43 2020 +0900
+++ b/filter.agda	Mon Jul 20 16:22:44 2020 +0900
@@ -173,20 +173,6 @@
 
 open _f⊆_
 
-_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 (f : Nat → Two) (p : PFunc ) : Set (suc n) where
-   field
-     gn  : Nat
-     f<n :  (f ↑ gn) f⊆ p
-
-open Gf
-
 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
        filter : L → Set n
@@ -206,6 +192,20 @@
 -- m≤m⊔n  = Data.Nat._⊔_
 open import Data.Nat.Properties
 
+_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 (f : Nat → Two) (p : PFunc ) : Set (suc n) where
+   field
+     gn  : Nat
+     f<n :  (f ↑ gn) f⊆ p
+
+open Gf
+
 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
 GF f = record {  
        filter = λ p → Gf f p