diff --git a/Data/Fin/Permutation.hs b/Data/Fin/Permutation.hs
new file mode 100644
--- /dev/null
+++ b/Data/Fin/Permutation.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where
+
+import Prelude (Functor (..), Applicative (..), Eq (..), Show (..), Bool (..), ($), (<$>), otherwise, flip, curry, uncurry)
+import Algebra
+import Control.Category (Category (..))
+import Data.Fin
+import Data.Fin.List hiding (swap)
+import Data.Foldable (elem, minimum, toList)
+import Data.Functor.Compose
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Monoid (Endo (..))
+import Data.Natural.Class (Natural (..))
+import qualified Data.Peano as P
+import Data.Universe.Class
+
+data Permutation n where
+    PZ :: Permutation P.Zero
+    PS :: Fin (P.Succ n) -> Permutation n -> Permutation (P.Succ n)
+
+deriving instance Eq (Permutation n)
+deriving instance Show (Permutation n)
+
+instance Natural n => Universe (Permutation n) where
+    universe = getCompose $ natural (Compose [PZ]) (Compose $ PS <$> toList enum <*> universe)
+
+instance Natural n => Finite (Permutation n)
+
+apply :: Permutation n -> List n a -> List n a
+apply PZ Nil = Nil
+apply (PS Zero p) (a:.as) = a:.apply p as
+apply (PS (Succ n) p) (a:.as) = uncurry (:.) $ at n (flip (,) a) (apply p as)
+
+unapply :: Permutation n -> List n a -> List n a
+unapply PZ Nil = Nil
+unapply (PS Zero p) (a:.as) = a:.unapply p as
+unapply (PS (Succ n) p) (a:.as) = unapply (PS Zero p) . uncurry (:.) $ at n (flip (,) a) as
+
+instance Natural n => Semigroup (Permutation n) where
+    (<>) = unOp₂ $ natural (Op₂ . curry $ \ (PZ, PZ) -> PZ) $ Op₂ . curry $ \ case
+        (PS m p, PS Zero q) -> PS m (p <> q)
+        (PS m p, PS (Succ n) q) -> let n' = unapply p enum !! n in case m of
+            Zero -> PS (Succ n') (p <> q)
+            Succ m' | m' == n'  -> PS Zero (p <> q)
+                    | otherwise -> PS (Succ n') (swap m' n' <> p <> q)
+
+instance Natural n => Monoid (Permutation n) where
+    mempty = natural PZ $ PS Zero mempty
+
+instance Natural n => Group (Permutation n) where
+    invert = appEndo . getCompose $ natural (Compose mempty) $ Compose . Endo $ \ case
+        PS Zero p -> PS Zero (invert p)
+        PS (Succ n) p -> let n' = apply p enum !! n in PS (Succ n') (invert p)
+
+swap :: Natural n => Fin n -> Fin n -> Permutation n
+swap = unOp₂ $ natural (Op₂ $ \ case) $ Op₂ . curry $ \ case
+    (Zero, Zero) -> mempty
+    (Succ m, Succ n) -> PS Zero (swap m n)
+    (Zero, Succ n) -> PS (Succ n) mempty
+    (Succ m, Zero) -> PS (Succ m) mempty
+
+newtype Op₂ a b n = Op₂ { unOp₂ :: a n -> a n -> b n }
+
+orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)
+orbit p n = case (!! n) <$> iterate (apply p) enum of
+    a:<as -> a:|takeWhile (/= a) as
+
+cycles :: ∀ n . Natural n => Permutation (P.Succ n) -> NonEmpty (NonEmpty (Fin (P.Succ n)))
+cycles p = nubOn minimum $ orbit p <$> case enum @(P.Succ n) of n:.ns -> n:|toList ns
+
+infixr 5 :<
+data Stream a = a :< Stream a
+  deriving (Functor)
+
+iterate :: (a -> a) -> a -> Stream a
+iterate f a = a :< (f <$> iterate f a)
+
+takeWhile :: (a -> Bool) -> Stream a -> [a]
+takeWhile f (a:<as) | f a = a:takeWhile f as
+                    | otherwise = []
+
+nubOn :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty a
+nubOn f (a:|as) = a:|go [f a] as
+  where go _ [] = []
+        go bs (a:as) | b `elem` bs = go bs as
+                     | otherwise   = a:go (b:bs) as
+          where b = f a
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright M Farkas-Dyck © 2018
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of M Farkas-Dyck nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,1 @@
+# permutations
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/permutations.cabal b/permutations.cabal
new file mode 100644
--- /dev/null
+++ b/permutations.cabal
@@ -0,0 +1,89 @@
+name:                permutations
+version:             0.1.0.0
+synopsis:            Permutations of finite sets
+-- description:
+license:             BSD3
+license-file:        LICENSE
+author:              M Farkas-Dyck
+maintainer:          strake888@gmail.com
+copyright:           2018 M Farkas-Dyck
+category:            Math
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      .
+  exposed-modules:     Data.Fin.Permutation
+  build-depends:       Fin >=0.2.1 && <0.3
+                     , alg >=0.2.5 && <0.3
+                     , base >= 4.7 && < 5
+                     , base-unicode-symbols
+                     , natural-induction >=0.2 && <0.3
+                     , peano >=0.1 && <0.2
+                     , universe-base >=1.0 && <1.1
+                     , util
+  default-language:    Haskell2010
+  default-extensions:  UnicodeSyntax
+                     , LambdaCase
+                     , EmptyCase
+                     , InstanceSigs
+                     , PartialTypeSignatures
+                     , ScopedTypeVariables
+                     , PolyKinds
+                     , DataKinds
+                     , ConstraintKinds
+                     , GADTs
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , StandaloneDeriving
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       ---Werror=incomplete-patterns
+                       ---Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods
+                       -Wno-unticked-promoted-constructors
+
+test-suite test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Main.hs
+  build-depends:       Fin >=0.2.1 && <0.3
+                     , alg >=0.2.5 && <0.3
+                     , base >=4.11 && <5
+                     , natural-induction >=0.2 && <0.3
+                     , peano >=0.1 && <0.2
+                     , smallcheck >=1.1.4
+                     , tasty >=1.0
+                     , tasty-smallcheck >=0.8
+                     , universe-base >=1.0 && <1.1
+                     , permutations
+  default-language:    Haskell2010
+  default-extensions:  UnicodeSyntax
+                     , LambdaCase
+                     , EmptyCase
+                     , InstanceSigs
+                     , PartialTypeSignatures
+                     , ScopedTypeVariables
+                     , PolyKinds
+                     , DataKinds
+                     , ConstraintKinds
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , MultiParamTypeClasses
+                     , StandaloneDeriving
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       -Werror=incomplete-patterns
+                       -Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods
+
+source-repository head
+  type:     git
+  location: https://github.com/strake/permutations.hs
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE TypeApplications, AllowAmbiguousTypes #-}
+
+module Main where
+
+import Algebra (Group (..))
+import Data.Fin (Fin, enum)
+import Data.Foldable (toList)
+import Data.Functor.Const
+import Data.List (nub)
+import Data.Natural.Class
+import Data.Peano (Peano (..))
+import Data.Universe.Class
+import qualified Numeric.Natural as N
+import Text.Printf
+
+import Test.SmallCheck.Series
+import Test.Tasty
+import Test.Tasty.SmallCheck
+
+import Data.Fin.Permutation
+
+main :: IO ()
+main = defaultMain . askOption $ \ (SmallCheckDepth d) -> 
+    let go :: ∀ n . Natural n => [TestTree]
+        go = tests @n : go @(Succ n)
+    in testGroup "" (take (d+1) $ go @Zero)
+
+tests :: ∀ n . Natural n => TestTree
+tests =
+    localOption (SmallCheckDepth (product [1..n])) $
+    testGroup (printf "n = %d" (n :: N.Natural))
+    [testGroup "universe"
+     [testProperty "size" $ length theUniverse == product [1..n],
+      testProperty "uniquity" $ nub theUniverse == theUniverse],
+     testProperty "mempty-preserves-apply" $ apply (mempty :: Permutation n) enum == enum,
+     testProperty "<>-mempty" $ \ (p :: Permutation n) -> p == p <> mempty && p == mempty <> p,
+     testProperty "<>-assoc" $ \ (p :: Permutation n) q r -> p <> (q <> r) == (p <> q) <> r,
+     testProperty "<>-preserves-apply" $ \ (p :: Permutation n) q -> (apply p . apply q) enum == apply (p <> q) enum,
+     testProperty "inverse" $ \ (p :: Permutation n) -> mempty == p <> invert p,
+     testProperty "invert . invert = id" $ \ (p :: Permutation n) -> p == (invert . invert) p,
+     testProperty "swap-self-inverse" $ \ m n -> let p = swap m n :: Permutation n in p == invert p]
+  where n :: Integral a => a
+        n = (fromIntegral . getConst) (reify :: Const Peano n)
+        theUniverse = universe @(Permutation n)
+
+instance (Monad m, Natural n) => Serial m (Fin n) where
+    series = generate $ \ d -> take (d+1) (toList enum)
+
+instance (Monad m, Natural n) => Serial m (Permutation n) where
+    series = generate $ \ d -> take (d+1) universe