diff --git a/src/Data/Permutation.idr b/src/Data/Permutation.idr
new file mode 100644
index 0000000..ef8d6ac
--- /dev/null
+++ b/src/Data/Permutation.idr
@@ -0,0 +1,26 @@
+module Data.Permutation
+
+import Data.Vect
+
+%default total
+
+
+public export
+Permutation : Nat -> Type
+Permutation n = Vect n (Fin n)
+
+
+public export
+identity : {n : _} -> Permutation n
+identity {n=Z} = []
+identity {n=S n} = FZ :: map FS identity
+
+public export
+reversed : {n : _} -> Permutation n
+reversed {n=Z} = []
+reversed {n=S n} = last :: map weaken reversed
+
+
+public export
+permuteVect : Permutation n -> Vect n a -> Vect n a
+permuteVect p v = map (\i => index i v) p