diff --git a/Data/Fin/List.hs b/Data/Fin/List.hs
--- a/Data/Fin/List.hs
+++ b/Data/Fin/List.hs
@@ -1,5 +1,5 @@
 module Data.Fin.List (Peano, List (..),
-                      fromList, uncons, head, tail, init, last, reverse, at, swap, (!!)) where
+                      fromList, uncons, head, tail, init, last, reverse, rotate, at, swap, (!!)) where
 
 import Prelude ()
 import Data.Fin.Private
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,83 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where
+
+import Prelude (Functor (..), Eq (..), Bool (..), ($), (<$>), otherwise, snd, flip, curry, uncurry)
+import Algebra
+import Control.Category (Category (..))
+import Data.Fin
+import Data.Fin.List hiding (swap)
+import qualified Data.Fin.List as L
+import Data.Foldable (elem, minimum, toList)
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Natural.Class (Natural (..))
+import qualified Data.Peano as P
+
+data Permutation n where
+    PZ :: Permutation P.Zero
+    PS :: Fin (P.Succ n) -> Permutation n -> Permutation (P.Succ 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 n q) -> case invert (PS n (invert p)) of
+            PS o r -> case (m, o) of
+                (Zero, _) -> PS o (r <> q)
+                (_, Zero) -> PS m (r <> q)
+                (Succ m, Succ o) -> PS (Succ o) (swap m o <> r <> q)
+
+instance Natural n => Monoid (Permutation n) where
+    mempty = natural PZ $ PS Zero mempty
+
+instance Natural n => Group (Permutation n) where
+    invert = snd . go
+      where
+        go :: ∀ n . Permutation n -> (List n (Fin n), Permutation n)
+        go PZ = (Nil, PZ)
+        go (PS n p) = (ms, PS m q)
+          where (ns, q) = go p
+                ms@(m:._) = L.swap Zero n $ Zero:.(Succ <$> ns)
+
+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/Data/Fin/Private.hs b/Data/Fin/Private.hs
--- a/Data/Fin/Private.hs
+++ b/Data/Fin/Private.hs
@@ -10,10 +10,12 @@
 import Data.Ap
 import Data.Eq
 import Data.Foldable
+import Data.Foldable1
 import Data.Function (on)
 import Data.Functor.Classes
 import Data.Functor.Compose
 import qualified Data.List as L
+import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe
 import Data.Monoid hiding ((<>))
 import Data.Natural.Class
@@ -156,6 +158,9 @@
 instance Natural n => Read1 (List n) where
     liftReadPrec rp rl = fromList <$> liftReadPrec rp rl >>= maybe empty pure
 
+instance Natural n => Foldable1 (List (P.Succ n)) where
+    toNonEmpty (a:.as) = a:|toList as
+
 uncons :: List (P.Succ n) a -> (a, List n a)
 uncons (x:.xs) = (x, xs)
 
@@ -176,6 +181,10 @@
 reverse :: List n a -> List n a
 reverse Nil = Nil
 reverse xs@(_:._) = liftA2 (:.) last (reverse . init) xs
+
+rotate :: Fin n -> List n a -> List n a
+rotate Zero as = as
+rotate (Succ n) as = rotate (inj₁ n) $ last as :. init as
 
 (!!) :: List n a -> Fin n -> a
 Nil !! n = case n of
diff --git a/Fin.cabal b/Fin.cabal
--- a/Fin.cabal
+++ b/Fin.cabal
@@ -1,5 +1,5 @@
 name:                Fin
-version:             0.2.3.0
+version:             0.2.4.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3
@@ -15,9 +15,12 @@
   build-depends:       peano
   exposed-modules:     Data.Fin
                      , Data.Fin.List
+                     , Data.Fin.Permutation
   other-modules:       Data.Ap
                      , Data.Fin.Private
-  build-depends:       base >=4.7 && <5
+  build-depends:       alg >=0.2.5 && <0.3
+                     , base >=4.7 && <5
+                     , foldable1 >=0.1 && <0.2
                      , natural-induction >=0.2 && <0.3
   default-language:    Haskell2010
   default-extensions:  UnicodeSyntax
@@ -31,4 +34,11 @@
                      , GADTs
                      , StandaloneDeriving
                      , DeriveFunctor, DeriveFoldable, DeriveTraversable
-  ghc-options:         -Wall -Wno-name-shadowing -Wno-unticked-promoted-constructors
+  ghc-options:         -Wall -Wcompat -Wredundant-constraints
+                       -Wincomplete-record-updates -Wincomplete-uni-patterns
+                       -Wno-name-shadowing -Wno-unticked-promoted-constructors
+                       -Werror=incomplete-patterns
+                       -Werror=incomplete-uni-patterns
+                       -Werror=incomplete-record-updates
+                       -Werror=missing-fields
+                       -Werror=missing-methods