diff --git a/lib/Quox/Context.idr b/lib/Quox/Context.idr
index 37a34d4..c566a4a 100644
--- a/lib/Quox/Context.idr
+++ b/lib/Quox/Context.idr
@@ -215,6 +215,13 @@ zipWith3Lazy : forall tm1, tm2, tm3, tm4.
 zipWith3Lazy f = zipWith3 $ \x, y, z => delay $ f x y z
 
 
+export
+unzip : Telescope (\i => (tm1 i, tm2 i)) from to ->
+        (Telescope tm1 from to, Telescope tm2 from to)
+unzip [<]             = ([<], [<])
+unzip (tel :< (x, y)) = let (xs, ys) = unzip tel in (xs :< x, ys :< y)
+
+
 export
 lengthPrf : Telescope _ from to -> Subset Nat (\len => len + from = to)
 lengthPrf [<]        = Element 0 Refl