diff --git a/Data/Fin.hs b/Data/Fin.hs
--- a/Data/Fin.hs
+++ b/Data/Fin.hs
@@ -1,3 +1,3 @@
-module Data.Fin (Fin (..), enum, inj₁, lift₁, fromFin, toFin, toFinMay) where
+module Data.Fin (Fin (..), enum, inj₁, proj₁, lift₁, fromFin, toFin, toFinMay) where
 
 import Data.Fin.Private
diff --git a/Data/Fin/Private.hs b/Data/Fin/Private.hs
--- a/Data/Fin/Private.hs
+++ b/Data/Fin/Private.hs
@@ -84,6 +84,14 @@
 inj₁ Zero = Zero
 inj₁ (Succ n) = Succ (inj₁ n)
 
+proj₁ :: Natural n => Fin (P.Succ n) -> Maybe (Fin n)
+proj₁ = unProj₁ $ natural (Proj₁ $ \ case Zero -> Nothing
+                                          Succ n -> case n of)
+                          (Proj₁ $ \ case Zero -> Just Zero
+                                          Succ n -> Succ <$> proj₁ n)
+
+newtype Proj₁ n = Proj₁ { unProj₁ :: Fin (P.Succ n) -> Maybe (Fin n) }
+
 lift₁ :: (Fin m -> Fin n) -> Fin (P.Succ m) -> Fin (P.Succ n)
 lift₁ _ Zero = Zero
 lift₁ f (Succ n) = Succ (f n)
diff --git a/Fin.cabal b/Fin.cabal
--- a/Fin.cabal
+++ b/Fin.cabal
@@ -1,5 +1,5 @@
 name:                Fin
-version:             0.2.6.1
+version:             0.2.7.0
 synopsis:            Finite totally-ordered sets
 -- description:         
 license:             BSD3