diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,10 @@
 # Revision history for natural-arithmetic
 
+## 0.1.3.0 -- 2022-05-23
+
+* Add strict variant of descend.
+* Add unboxed Fin type
+
 ## 0.1.2.0 -- 2019-01-20
 
 * Add strict variant of descend.
diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal
--- a/natural-arithmetic.cabal
+++ b/natural-arithmetic.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.2
 name: natural-arithmetic
-version: 0.1.2.0
+version: 0.1.3.0
 synopsis: Arithmetic of natural numbers
 description:
   A search for terms like `arithmetic` and `natural` on hackage reveals
@@ -74,7 +74,7 @@
     Arithmetic.Types
     Arithmetic.Unsafe
     Arithmetic.Plus
-  build-depends: base>=4.11 && <5
+  build-depends: base>=4.14 && <5
   hs-source-dirs: src
   default-language: Haskell2010
   ghc-options: -Wall -O2
diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs
--- a/src/Arithmetic/Fin.hs
+++ b/src/Arithmetic/Fin.hs
@@ -3,6 +3,7 @@
 {-# language ExplicitNamespaces #-}
 {-# language GADTs #-}
 {-# language KindSignatures #-}
+{-# language MagicHash #-}
 {-# language ScopedTypeVariables #-}
 {-# language TypeApplications #-}
 {-# language TypeOperators #-}
@@ -35,12 +36,16 @@
   , absurd
     -- * Demote
   , demote
+    -- * Lift and Unlift
+  , lift
+  , unlift
   ) where
 
 import Prelude hiding (last)
 
 import Arithmetic.Nat ((<?))
 import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))
+import GHC.Exts (Int(I#))
 import GHC.TypeNats (type (+))
 
 import qualified Arithmetic.Lt as Lt
@@ -48,20 +53,24 @@
 import qualified Arithmetic.Equal as Eq
 import qualified Arithmetic.Nat as Nat
 import qualified Arithmetic.Plus as Plus
+import qualified Arithmetic.Unsafe as Unsafe
 
 -- | Raise the index by @m@ and weaken the bound by @m@, adding
 -- @m@ to the right-hand side of @n@.
 incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)
+{-# inline incrementR #-}
 incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf)
 
 -- | Raise the index by @m@ and weaken the bound by @m@, adding
 -- @m@ to the left-hand side of @n@.
 incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n)
+{-# inline incrementL #-}
 incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf)
 
 -- | Weaken the bound by @m@, adding it to the left-hand side of
 -- the existing bound. This does not change the index.
 weakenL :: forall n m. Fin n -> Fin (m + n)
+{-# inline weakenL #-}
 weakenL (Fin i pf) = Fin i
   ( Lt.substituteR
     (Plus.commutative @n @m)
@@ -71,15 +80,18 @@
 -- | Weaken the bound by @m@, adding it to the right-hand side of
 -- the existing bound. This does not change the index.
 weakenR :: forall n m. Fin n -> Fin (n + m)
+{-# inline weakenR #-}
 weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero)
 
 -- | Weaken the bound, replacing it by another number greater than
 -- or equal to itself. This does not change the index.
 weaken :: forall n m. (n <= m) -> Fin n -> Fin m
+{-# inline weaken #-}
 weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)
 
 -- | A finite set of no values is impossible.
 absurd :: Fin 0 -> void
+{-# inline absurd #-}
 absurd (Fin _ pf) = Lt.absurd pf
 
 -- | Fold over the numbers bounded by @n@ in descending
@@ -325,4 +337,13 @@
 -- at a boundary where a safe interface meets the unsafe primitives
 -- on top of which it is built.
 demote :: Fin n -> Int
+{-# inline demote #-}
 demote (Fin i _) = Nat.demote i
+
+lift :: Unsafe.Fin# n -> Fin n
+{-# inline lift #-}
+lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt
+
+unlift :: Fin n -> Unsafe.Fin# n
+{-# inline unlift #-}
+unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i
diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs
--- a/src/Arithmetic/Nat.hs
+++ b/src/Arithmetic/Nat.hs
@@ -42,19 +42,23 @@
 
 -- | Infix synonym of 'testLessThan'.
 (<?) :: Nat a -> Nat b -> Maybe (a < b)
+{-# inline (<?) #-}
 (<?) = testLessThan
 
 -- | Infix synonym of 'testLessThanEqual'.
 (<=?) :: Nat a -> Nat b -> Maybe (a <= b)
+{-# inline (<=?) #-}
 (<=?) = testLessThanEqual
 
 -- | Infix synonym of 'testEqual'.
 (=?) :: Nat a -> Nat b -> Maybe (a :=: b)
+{-# inline (=?) #-}
 (=?) = testEqual
 
 -- | Is the first argument strictly less than the second
 -- argument?
 testLessThan :: Nat a -> Nat b -> Maybe (a < b)
+{-# inline testLessThan #-}
 testLessThan (Nat x) (Nat y) = if x < y
   then Just Lt
   else Nothing
@@ -62,28 +66,33 @@
 -- | Is the first argument less-than-or-equal-to the second
 -- argument?
 testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)
+{-# inline testLessThanEqual #-}
 testLessThanEqual (Nat x) (Nat y) = if x <= y
   then Just Lte
   else Nothing
 
 -- | Are the two arguments equal to one another?
 testEqual :: Nat a -> Nat b -> Maybe (a :=: b)
+{-# inline testEqual #-}
 testEqual (Nat x) (Nat y) = if x == y
   then Just Eq
   else Nothing
 
 -- | Is zero equal to this number or less than it?
 testZero :: Nat a -> Either (0 :=: a) (0 < a)
+{-# inline testZero #-}
 testZero (Nat x) = case x of
   0 -> Left Eq
   _ -> Right Lt
 
 -- | Add two numbers.
 plus :: Nat a -> Nat b -> Nat (a + b)
+{-# inline plus #-}
 plus (Nat x) (Nat y) = Nat (x + y)
 
 -- | The successor of a number.
 succ :: Nat a -> Nat (a + 1)
+{-# inline succ #-}
 succ n = plus n one
 
 -- | Subtract the second argument from the first argument.
@@ -95,30 +104,36 @@
 
 -- | The number zero.
 zero :: Nat 0
+{-# inline zero #-}
 zero = Nat 0
 
 -- | The number one.
 one :: Nat 1
+{-# inline one #-}
 one = Nat 1
 
 -- | The number two.
 two :: Nat 2
+{-# inline two #-}
 two = Nat 2
 
 -- | The number three.
 three :: Nat 3
+{-# inline three #-}
 three = Nat 3
 
 -- | Use GHC's built-in type-level arithmetic to create a witness
 -- of a type-level number. This only reduces if the number is a
 -- constant.
 constant :: forall n. KnownNat n => Nat n
+{-# inline constant #-}
 constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))
 
 -- | Extract the 'Int' from a 'Nat'. This is intended to be used
 -- at a boundary where a safe interface meets the unsafe primitives
 -- on top of which it is built.
 demote :: Nat n -> Int
+{-# inline demote #-}
 demote (Nat n) = n
 
 -- | Run a computation on a witness of a type-level number. The
@@ -126,4 +141,5 @@
 -- not checked. Failure to upload this invariant will lead to a
 -- segfault.
 with :: Int -> (forall n. Nat n -> a) -> a
+{-# inline with #-}
 with i f = f (Nat i)
diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs
--- a/src/Arithmetic/Unsafe.hs
+++ b/src/Arithmetic/Unsafe.hs
@@ -4,12 +4,15 @@
 {-# language GADTSyntax #-}
 {-# language GeneralizedNewtypeDeriving #-}
 {-# language KindSignatures #-}
+{-# language MagicHash #-}
 {-# language RoleAnnotations #-}
 {-# language StandaloneDeriving #-}
 {-# language TypeOperators #-}
+{-# language UnliftedNewtypes #-}
 
 module Arithmetic.Unsafe
   ( Nat(..)
+  , Fin#(..)
   , type (<)(Lt)
   , type (<=)(Lte)
   , type (:=:)(Eq)
@@ -19,6 +22,7 @@
 
 import Control.Category (Category)
 import Data.Kind (Type)
+import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep))
 
 import qualified Control.Category
 import qualified GHC.TypeNats as GHC
@@ -38,6 +42,10 @@
 type role Nat nominal
 
 deriving newtype instance Show (Nat n)
+
+-- | Finite numbers without the overhead of carrying around a proof.
+newtype Fin# :: GHC.Nat -> TYPE 'IntRep where
+  Fin# :: Int# -> Fin# n
 
 -- | Proof that the first argument is strictly less than the
 -- second argument.