diff --git a/lib/Quox/Syntax/Dim.idr b/lib/Quox/Syntax/Dim.idr
index 0f90b35..6d8ea7e 100644
--- a/lib/Quox/Syntax/Dim.idr
+++ b/lib/Quox/Syntax/Dim.idr
@@ -132,3 +132,8 @@ DecEq (Dim d) where
 public export %inline
 BV : (i : Nat) -> (0 _ : LT i d) => Dim d
 BV i = B $ V i
+
+
+export
+weakD : {default 1 by : Nat} -> Dim d -> Dim (by + d)
+weakD p = p // shift by