diff --git a/Data/Fin.hs b/Data/Fin.hs
deleted file mode 100644
--- a/Data/Fin.hs
+++ /dev/null
@@ -1,99 +0,0 @@
-{-# LANGUAGE TypeApplications #-}
-
-module Data.Fin where
-
-import Prelude hiding (iterate)
-import Control.Applicative
-import Data.Ap
-import Data.CList (CList (..))
-import Data.Foldable
-import Data.Function (on)
-import Data.Functor.Compose
-import Data.Maybe
-import Data.Natural.Class
-import Data.Peano (Peano)
-import qualified Data.Peano as P
-import Data.Semigroup (Endo (..))
-import qualified Numeric.Natural as N
-import qualified Text.ParserCombinators.ReadP as Read
-import Text.ParserCombinators.ReadPrec (readP_to_Prec)
-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)
-deriving instance Show (Fin n)
-
-instance Read (Fin P.Zero) where readPrec = empty
-instance Read (Fin n) => Read (Fin (P.Succ n)) where
-    readPrec = Succ <$ string "Succ" <*> readPrec <|> Zero <$ string "Zero"
-      where string = readP_to_Prec . pure . Read.string
-
-instance Bounded (Fin (P.Succ P.Zero)) where
-    minBound = Zero
-    maxBound = Zero
-
-instance Bounded (Fin n) => Bounded (Fin (P.Succ n)) where
-    minBound = Zero
-    maxBound = Succ maxBound
-
-instance Enum (Fin P.Zero) where
-    toEnum _ = error "toEnum @(Fin Zero)"
-    fromEnum = \ case
-    succ = \ case
-    pred = \ case
-
-instance (Natural n, Enum (Fin n)) => Enum (Fin (P.Succ n)) where
-    toEnum 0 = Zero
-    toEnum n = Succ (toEnum (pred n))
-    fromEnum Zero = 0
-    fromEnum (Succ n) = succ (fromEnum n)
-    enumFrom Zero = Zero : (Succ <$> toList enum)
-    enumFrom (Succ n) = (tail . enumFrom . inj₁) n
-
-enum :: Natural n => CList n (Fin n)
-enum = ap $ natural (Ap Nil) (Ap (Zero :. (Succ <$> enum)))
-
-instance Num (Fin P.Zero) where
-    (+) = \ case
-    (*) = \ case
-    abs = id
-    negate = \ case
-    signum = \ case
-    fromInteger _ = error "fromInteger @(Fin Zero)"
-
-instance (Natural n, Num (Fin n)) => Num (Fin (P.Succ n)) where
-    a + b = toFin $ ((+) @N.Natural `on` fromFin) a b
-    a - b = toFin $ ((-) @  Integer `on` fromFin) a b
-    a * b = toFin $ ((*) @N.Natural `on` fromFin) a b
-
-    abs = id
-    signum = lift₁ . appEndo . getCompose $
-             natural @n (Compose . Endo $ \ case) (Compose . Endo $ pure Zero)
-
-    fromInteger = toFin
-
-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))
diff --git a/Fin.cabal b/Fin.cabal
--- a/Fin.cabal
+++ b/Fin.cabal
@@ -1,5 +1,5 @@
 name:                Fin
-version:             0.1.1.0
+version:             0.2.0.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3