--- a/limit-to.agda	Wed May 13 13:28:16 2015 +0900
+++ b/limit-to.agda	Fri Jun 26 17:56:22 2015 +0900
@@ -10,6 +10,9 @@
 open import Category.Sets
 open Functor
 
+open import Data.Nat hiding ( _⊔_ ) renaming ( suc to succ )
+open import Data.Bool
+
 
 -- If we have limit then we have equalizer                                                                                                                                                                  
 ---  two objects category
@@ -22,22 +25,30 @@
 
 postulate φ id-0 id-1 f g : Set  c₂
 
-
 infixr 40 _::_
 data  List {a} (A : Set a)  : Set a where
    [] : List A
    _::_ : A -> List A -> List A
 
-data  Maybe  {a} (A : Set a)  : Set a where
-   nothing : Maybe A
-   just : A -> Maybe A
+nat-equal : ℕ -> ℕ -> Bool
+nat-equal zero zero = true
+nat-equal (succ _) zero = false
+nat-equal zero (succ _) = false
+nat-equal (succ x) (succ y) = nat-equal x y
 
-memberp1 : {a : Level } -> {A : Set a} → A → List A → {!!} -> Maybe A
-memberp1 = {!!}
+memberp :  ℕ  ->  List  ℕ  → Bool
+memberp _ []  = false
+memberp x (y :: T) with nat-equal x y
+... | true = true
+... | false = memberp x T
 
-memberp : {a : Level } -> {A : Set a} → A → List A → Maybe A
-memberp _ []  = nothing
-memberp x ( H :: T ) = memberp1 x T ( x ≡ H )
+memberp1 :  ℕ  ->  List  ℕ  → Bool
+memberp1 _ []  = false
+memberp1 x (y :: T) with compare x y
+memberp1 x (.x :: T)  | equal .x = true
+memberp1 x ( .(succ (x + y)) :: T)  | less .x y = memberp1 x T
+memberp1 .(succ (x + y)) ( x :: T)  | greater .x y = memberp1 x T
+