diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
new file mode 100644
index 0000000..5a2be43
--- /dev/null
+++ b/src/Data/Fin.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeInType            #-}
+{-# LANGUAGE StandaloneDeriving    #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE NoImplicitPrelude     #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE QuasiQuotes           #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE UnicodeSyntax         #-}
+
+-- | Finite types
+module Data.Fin where
+
+import Data.Singletons.TH
+import Data.TypeClass      (Eq, Show)
+import Data.Kind           (Type)
+import Data.Nat
+
+
+-- | Fin n is a type with n inhabitants
+data Fin ∷ ℕ → Type where
+  Zero ∷ Fin (S n)         -- ^ Type with no inhabitants
+  Suc  ∷ Fin n → Fin (S n) -- ^ Suc construct a type with n+1 inhabitants
+
+
+deriving instance Eq (Fin n)
+
+deriving instance Show (Fin n)
+
+
+-- * Conversions
+
+-- | Convert a finite set to a natural
+toℕ ∷ Fin n → ℕ
+toℕ Zero    = Z
+toℕ (Suc n) = S (toℕ n)
+
+
+-- | Convert a natural to a finite set
+fromℕ ∷ Sℕ n → Fin (S n)
+fromℕ SZ     = Zero
+fromℕ (SS n) = Suc (fromℕ n)