diff --git a/Cubical/Data/Maybe/Base.agda b/Cubical/Data/Maybe/Base.agda
index 0f230b6233..1712b822ca 100644
--- a/Cubical/Data/Maybe/Base.agda
+++ b/Cubical/Data/Maybe/Base.agda
@@ -5,8 +5,9 @@ open import Cubical.Core.Everything
 
 private
   variable
-    ℓ : Level
-    A B : Type ℓ
+    ℓ ℓA ℓB : Level
+    A : Type ℓA
+    B : Type ℓB
 
 data Maybe (A : Type ℓ) : Type ℓ where
   nothing : Maybe A
@@ -23,3 +24,7 @@ map-Maybe f (just x) = just (f x)
 rec : B → (A → B) → Maybe A → B
 rec n j nothing = n
 rec n j (just a) = j a
+
+elim : ∀ {A : Type ℓA} (B : Maybe A → Type ℓB) → B nothing → ((x : A) → B (just x)) → (mx : Maybe A) → B mx
+elim B n j nothing = n
+elim B n j (just a) = j a