--- a/src/filter.agda	Tue Mar 15 14:09:20 2022 +0900
+++ b/src/filter.agda	Tue Mar 15 15:46:39 2022 +0900
@@ -149,6 +149,18 @@
 --     L have to be a Latice
 --
 
+record IsPOder  {n : Level} (P : Set n) (_p≤_ : P → P → Set n) (1p : P) : Set n where
+   field
+     1p-max : { x : P } → x p≤ 1p
+     p<trans : { x y z : P } → x p≤ y → y p≤ z → x p≤ z 
+     p<refl : { x  : P } → x p≤ x 
+
+record POder {n : Level} (P : Set n) : Set (suc n) where
+   field
+     _p≤_ : P → P → Set n
+     1p : P 
+     isPOder : IsPOder P _p≤_ 1p
+
 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