diff --git a/Data/Ap.hs b/Data/Ap.hs
new file mode 100644
--- /dev/null
+++ b/Data/Ap.hs
@@ -0,0 +1,3 @@
+module Data.Ap where
+
+newtype Ap f x a = Ap { ap :: f a (x a) }
diff --git a/Data/Fin.hs b/Data/Fin.hs
new file mode 100644
--- /dev/null
+++ b/Data/Fin.hs
@@ -0,0 +1,3 @@
+module Data.Fin (Fin (..), enum, inj₁, lift₁, fromFin, toFin, toFinMay) where
+
+import Data.Fin.Private
diff --git a/Data/Fin/List.hs b/Data/Fin/List.hs
new file mode 100644
--- /dev/null
+++ b/Data/Fin/List.hs
@@ -0,0 +1,6 @@
+module Data.Fin.List (Peano, List (..),
+                      fromList, uncons, head, tail, init, last, reverse, (!!)) where
+
+import Prelude ()
+import Data.Fin.Private
+import Data.Peano
diff --git a/Data/Fin/Private.hs b/Data/Fin/Private.hs
new file mode 100644
--- /dev/null
+++ b/Data/Fin/Private.hs
@@ -0,0 +1,184 @@
+{-# LANGUAGE TypeApplications #-}
+
+module Data.Fin.Private where
+
+import Prelude (Functor (..), Show (..), Num (..), Enum (..), Bounded (..), Integral (..), Bool (..), Integer, ($), (&&), fst, snd, error)
+import Control.Applicative
+import Control.Arrow (Kleisli (..))
+import Control.Category
+import Control.Monad (Monad (..))
+import Data.Ap
+import Data.Eq
+import Data.Foldable
+import Data.Function (on)
+import Data.Functor.Classes
+import Data.Functor.Compose
+import qualified Data.List as L
+import Data.Maybe
+import Data.Monoid hiding ((<>))
+import Data.Natural.Class
+import Data.Ord
+import Data.Peano (Peano)
+import qualified Data.Peano as P
+import Data.Semigroup (Semigroup (..))
+import Data.Traversable
+import Data.Typeable
+import qualified Numeric.Natural as N
+import Text.Read (Read (..))
+
+data Fin :: Peano -> * where
+    Zero :: Fin (P.Succ n)
+    Succ :: Fin n -> Fin (P.Succ n)
+
+deriving instance Eq (Fin n)
+deriving instance Ord (Fin n)
+
+instance Show (Fin n) where show = show . fromFin @N.Natural
+
+instance Read (Fin P.Zero) where readPrec = empty
+instance (Natural n, Read (Fin n)) => Read (Fin (P.Succ n)) where
+    readPrec = toFinMay <$> readPrec @N.Natural >>= maybe empty pure
+
+instance Natural n => Bounded (Fin (P.Succ n)) where
+    minBound = Zero
+    maxBound = getCompose $ natural (Compose Zero) (Compose maxBound)
+
+instance Natural n => Enum (Fin n) where
+    toEnum n = natural (error "toEnum @(Fin Zero)") $ case n of
+        0 -> Zero
+        _ -> Succ (toEnum (pred n))
+    fromEnum = unFlip . getCompose $ natural (Compose . Flip $ \ case) $ Compose . Flip $ \ case
+        Zero -> 0
+        Succ n -> succ (fromEnum n)
+    succ = unJoin . getCompose $ natural (Compose . Join $ \ case) $ Compose . Join $ \ case
+        Zero -> toEnum 1
+        Succ n -> Succ (succ n)
+    pred = unJoin . getCompose $ natural (Compose . Join $ \ case) $ Compose . Join $ \ case
+        Zero -> error "pred 0"
+        Succ n -> inj₁ n
+    enumFrom = runKleisli . unJoin . getCompose $ natural (Compose . Join . Kleisli $ \ case) $ Compose . Join . Kleisli @[] $ \ case
+        Zero -> Zero : (Succ <$> toList enum)
+        Succ n -> (L.tail . enumFrom . inj₁) n
+
+newtype Join s a = Join { unJoin :: s a a }
+
+enum :: Natural n => List n (Fin n)
+enum = ap $ natural (Ap Nil) (Ap (Zero :. (Succ <$> enum)))
+
+instance Natural n => Num (Fin n) where
+    (+) = unJoin₂ . getCompose $ natural (Compose . Join₂ $ \ case) $ Compose . Join₂ $ \ a b -> toFin $ ((+) @N.Natural `on` fromFin) a b
+    (-) = unJoin₂ . getCompose $ natural (Compose . Join₂ $ \ case) $ Compose . Join₂ $ \ a b -> toFin $ ((-) @  Integer `on` fromFin) a b
+    (*) = unJoin₂ . getCompose $ natural (Compose . Join₂ $ \ case) $ Compose . Join₂ $ \ a b -> toFin $ ((*) @N.Natural `on` fromFin) a b
+    abs = id
+    negate = unJoin . getCompose $ natural (Compose . Join $ \ case) $ Compose . Join $ \ a -> toFin $ (negate @Integer . fromFin) a
+    signum = unJoin . getCompose $ natural (Compose . Join $ \ case) $ Compose . Join $ \ case
+        Zero -> Zero
+        Succ _ -> toFin (1 :: N.Natural)
+    fromInteger n = natural (error "fromInteger @(Fin Zero)") (toFin n)
+
+newtype Join₂ s a = Join₂ { unJoin₂ :: s a (s a a) }
+
+inj₁ :: Fin n -> Fin (P.Succ n)
+inj₁ Zero = Zero
+inj₁ (Succ n) = Succ (inj₁ n)
+
+lift₁ :: (Fin m -> Fin n) -> Fin (P.Succ m) -> Fin (P.Succ n)
+lift₁ _ Zero = Zero
+lift₁ f (Succ n) = Succ (f n)
+
+fromFin :: Integral a => Fin n -> a
+fromFin Zero = 0
+fromFin (Succ n) = succ (fromFin n)
+
+toFin :: ∀ n a . (Natural n, Integral a) => a -> Fin (P.Succ n)
+toFin = fromJust . toFinMay . (`mod` getConst (iterate @n (+1) 1))
+
+toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin (P.Succ n))
+toFinMay = getCompose . getCompose . getCompose $
+           natural (Compose . Compose . Compose $ \ case 0 -> Just Zero
+                                                         _ -> Nothing)
+                   (Compose . Compose . Compose $ \ case 0 -> Just Zero
+                                                         n -> Succ <$> toFinMay (n-1))
+
+infixr 5 :.
+data List n a where
+    Nil :: List P.Zero a
+    (:.) :: a -> List n a -> List (P.Succ n) a
+
+deriving instance (Eq   a) => Eq   (List n a)
+deriving instance (Ord  a) => Ord  (List n a)
+deriving instance Functor     (List n)
+deriving instance Foldable    (List n)
+deriving instance Traversable (List n)
+deriving instance Typeable List
+
+instance Show a => Show (List n a) where
+    showsPrec = showsPrec1
+
+instance (Read a, Natural n) => Read (List n a) where
+    readPrec = readPrec1
+
+fromList :: Natural n => [a] -> Maybe (List n a)
+fromList = t $ natural (T $ \ case [] -> Just Nil
+                                   _  -> Nothing)
+                       (T $ \ case [] -> Nothing
+                                   x:xs -> (x:.) <$> fromList xs)
+
+newtype T a n = T { t :: [a] -> Maybe (List n a) }
+
+instance Semigroup a => Semigroup (List n a) where
+    Nil <> Nil = Nil
+    (x:.xs) <> (y:.ys) = x<>y:.xs<>ys
+
+instance (Natural n, Semigroup a, Monoid a) => Monoid (List n a) where
+    mempty = unFlip $ natural (Flip Nil) (Flip $ mempty:.mempty)
+    mappend = (<>)
+
+instance Natural n => Applicative (List n) where
+    pure a = unFlip $ natural (Flip Nil) (Flip $ a:.pure a)
+    (<*>) = unS $ natural (S $ \ Nil Nil -> Nil)
+                          (S $ \ (f:.fs) (x:.xs) -> f x :. (fs <*> xs))
+
+newtype Flip f a b = Flip { unFlip :: f b a }
+
+newtype S a b n = S { unS :: List n (a -> b) -> List n a -> List n b }
+
+instance Eq1 (List n) where
+    liftEq _ Nil Nil = True
+    liftEq (==) (x:.xs) (y:.ys) = x == y && liftEq (==) xs ys
+
+instance Ord1 (List n) where
+    liftCompare _ Nil Nil = EQ
+    liftCompare cmp (x:.xs) (y:.ys) = cmp x y <> liftCompare cmp xs ys
+
+instance Show1 (List n) where
+    liftShowsPrec sp sl n = liftShowsPrec sp sl n . toList
+
+instance Natural n => Read1 (List n) where
+    liftReadPrec rp rl = fromList <$> liftReadPrec rp rl >>= maybe empty pure
+
+uncons :: List (P.Succ n) a -> (a, List n a)
+uncons (x:.xs) = (x, xs)
+
+head :: List (P.Succ n) a -> a
+head = fst . uncons
+
+tail :: List (P.Succ n) a -> List n a
+tail = snd . uncons
+
+init :: List (P.Succ n) a -> List n a
+init (_:.Nil)       = Nil
+init (x:.xs@(_:._)) = x:.init xs
+
+last :: List (P.Succ n) a -> a
+last (x:.Nil) = x
+last (_:.xs@(_:._)) = last xs
+
+reverse :: List n a -> List n a
+reverse Nil = Nil
+reverse xs@(_:._) = liftA2 (:.) last (reverse . init) xs
+
+(!!) :: List n a -> Fin n -> a
+Nil !! n = case n of
+(x:._)  !! Zero = x
+(_:.xs) !! Succ n = xs !! n
diff --git a/Fin.cabal b/Fin.cabal
--- a/Fin.cabal
+++ b/Fin.cabal
@@ -1,5 +1,5 @@
 name:                Fin
-version:             0.2.0.0
+version:             0.2.1.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3
@@ -14,18 +14,21 @@
 library
   build-depends:       peano
   exposed-modules:     Data.Fin
+                     , Data.Fin.List
+  other-modules:       Data.Ap
+                     , Data.Fin.Private
   build-depends:       base >=4.7 && <5
-                     , clist >=0.2 && <0.3
                      , natural-induction >=0.2 && <0.3
   default-language:    Haskell2010
   default-extensions:  UnicodeSyntax
-                     , ScopedTypeVariables
                      , LambdaCase
                      , EmptyCase
+                     , ScopedTypeVariables
+                     , FlexibleContexts
+                     , FlexibleInstances
                      , PolyKinds
                      , DataKinds
                      , GADTs
-                     , FlexibleContexts
-                     , FlexibleInstances
                      , StandaloneDeriving
-  ghc-options:         -Wall -Wno-unticked-promoted-constructors
+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable
+  ghc-options:         -Wall -Wno-name-shadowing -Wno-unticked-promoted-constructors
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2017, M Farkas-Dyck
+Copyright © 2017, M Farkas-Dyck
 
 All rights reserved.