diff --git a/stdlib/list.quox b/stdlib/list.quox
index 5b34ee4..feaa0a7 100644
--- a/stdlib/list.quox
+++ b/stdlib/list.quox
@@ -240,6 +240,9 @@ def0 ZipWith = zip-with.Result
 def zip-with-het = zip-with.zip-with-het
 def zip-with-hetω = zip-with.zip-with-hetω
 
+def map : 0.(A B : ★) → ω.(A → B) → (n : ℕ) → Vec n A → Vec n B =
+  λ A B f ⇒ elim A (λ n _ ⇒ Vec n B) 'nil (λ x _ _ ys ⇒ (f x, ys))
+
 #[compile-scheme "(lambda% (n xs) xs)"]
 def up : 0.(A : ★) → (n : ℕ) → Vec n A → Vec¹ n A =
   λ A n ⇒