diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md
index 77bebf3..5ca50cf 100644
--- a/src/Monad/Instance/K/Instance/Maybe.lagda.md
+++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md
@@ -48,16 +48,12 @@ module _ {c ℓ' : Level} where
   open Equiv
   -- open Setoid
 
-  private
-    variable
-      a : Level
-
-  data Maybe (A : Set a) : Set a where
+  data Maybe {a} (A : Set a) : Set a where
     nothing : Maybe A
     just : A → Maybe A
 
-  maybeSetoid : ∀ (A : Set a) → Setoid' a a
-  maybeSetoid A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
+  maybeSetoid : ∀ {a} (A : Set a) → Setoid' a a
+  maybeSetoid {a} A = record { Carrier = Maybe A ; _≈_ = eq ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } }
     where
       eq : Maybe A → Maybe A → Set a
       eq nothing nothing = ⊤ₚ
@@ -83,6 +79,8 @@ module _ {c ℓ' : Level} where
       trans' {just x} {just y} {just z} = trans-≡
   
   -- maybe-η : 
+  lift-maybe : ∀ {a} (A : Set a) (x : A) → Maybe A
+  lift-maybe {a} A x = just x
 
   -- TODO this is completely wrong...
   maybe : Monad Setoids