diff --git a/Data/Fin.hs b/Data/Fin.hs
--- a/Data/Fin.hs
+++ b/Data/Fin.hs
@@ -1,10 +1,99 @@
-{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
+{-# 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.0.0
+version:             0.1.1.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3
@@ -14,6 +14,18 @@
 library
   build-depends:       peano
   exposed-modules:     Data.Fin
-  other-extensions:    GADTs, KindSignatures, DataKinds
   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
+                     , PolyKinds
+                     , DataKinds
+                     , GADTs
+                     , FlexibleContexts
+                     , FlexibleInstances
+                     , StandaloneDeriving
+  ghc-options:         -Wall -Wno-unticked-promoted-constructors