Maybe: elim. (#751)

Co-authored-by: Andreas Nuyts <[email protected]>
agda · Apr 3, 2022 · eee5c9c · eee5c9c
1 parent ab79d25
commit eee5c9c
Showing 1 changed file with 7 additions and 2 deletions.
diff --git 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