diff --git a/Data/Fin.hs b/Data/Fin.hs
--- a/Data/Fin.hs
+++ b/Data/Fin.hs
@@ -1,3 +1,11 @@
-module Data.Fin (Fin (..), enum, inj₁, proj₁, lift₁, fromFin, toFin, toFinMay) where
+module Data.Fin (Fin (..), enum, inj₁, proj₁, lift₁, fromFin, toFin, toFinMay, pred) where
 
+import Prelude ()
+import Data.Maybe (Maybe (..))
 import Data.Fin.Private
+import qualified Data.Peano as P
+
+pred :: Fin (P.Succ n) -> Maybe (Fin n)
+pred = \ case
+    Zero -> Nothing
+    Succ n -> Just n
diff --git a/Data/Fin/Private.hs b/Data/Fin/Private.hs
--- a/Data/Fin/Private.hs
+++ b/Data/Fin/Private.hs
@@ -14,6 +14,7 @@
 import Data.Function (on)
 import Data.Functor.Classes
 import Data.Functor.Compose
+import Data.Kind (Type)
 import qualified Data.List as L
 import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe
@@ -28,7 +29,7 @@
 import qualified Numeric.Natural as N
 import Text.Read (Read (..))
 
-data Fin :: Peano -> * where
+data Fin :: Peano -> Type where
     Zero :: Fin (P.Succ n)
     Succ :: Fin n -> Fin (P.Succ n)
 
@@ -139,7 +140,7 @@
     Nil <> Nil = Nil
     (x:.xs) <> (y:.ys) = x<>y:.xs<>ys
 
-instance (Natural n, Semigroup a, Monoid a) => Monoid (List n a) where
+instance (Natural n, Monoid a) => Monoid (List n a) where
     mempty = unFlip $ natural (Flip Nil) (Flip $ mempty:.mempty)
     mappend = (<>)
 
diff --git a/Fin.cabal b/Fin.cabal
--- a/Fin.cabal
+++ b/Fin.cabal
@@ -1,5 +1,5 @@
 name:                Fin
-version:             0.2.7.0
+version:             0.2.8.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain