PermutationFunsHigherKinded.idr

import Data.Vect
import Data.Fin

%default total

fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins

Permutation : Nat -> Type
Permutation n = {a : Type} -> Vect n a -> Vect n a

permutations : {n : Nat} -> Vect (fact n) (Permutation n)
permutations {n = Z} = [id]
permutations {n = S n} =
    rewrite multCommutative (S n) (fact n) in
    concat . map inserts $ permutations {n = n}
  where
    inserts : Permutation k -> Vect (S k) (Permutation (S k))
    inserts pi = map (\i => \(x :: xs) => insertAt i x . pi $ xs) fins