diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,16 @@
 # Changelog for the `parameterized-utils` package
 
+## 2.3.0.0 -- 2026-03-06
+
+  * BREAKING: Remove the `Iso`s `fin0Void`, `fin1Unit`, and `fin2Bool`.
+  * Deprecate `Data.Parameterized.Compose`.
+
+## 2.2.0.0 -- 2026-01-22
+
+  * Replace dependency on `lens` with `microlens` and `microlens-pro`.
+  * Deprecate the `Iso`s `fin0Void`, `fin1Unit`, and `fin2Bool`.
+  * Add `fin0Absurd :: Fin 0 -> a`.
+
 ## 2.1.11.0 -- *2025 Nov 4*
 
   * Add support for GHC 9.12.
diff --git a/parameterized-utils.cabal b/parameterized-utils.cabal
--- a/parameterized-utils.cabal
+++ b/parameterized-utils.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          parameterized-utils
-Version:       2.1.11.0
+Version:       2.3.0.0
 Author:        Galois Inc.
 Maintainer:    kquick@galois.com, rscott@galois.com
 stability:     stable
@@ -59,9 +59,8 @@
                , hashable       >=1.2  && <1.6
                , hashtables     >=1.2  && <1.5
                , indexed-traversable
-               , lens           >=4.16 && <5.4
+               , microlens      >=0.5 && <0.6
                , mtl
-               , profunctors    >=5.6 && < 5.7
                , template-haskell
                , text
                , vector         >=0.12 && < 0.14
@@ -136,7 +135,7 @@
                , hashtables
                , hedgehog
                , indexed-traversable
-               , lens
+               , microlens >=0.5 && <0.6
                , mtl
                , parameterized-utils
                , tasty >= 1.2 && < 1.6
diff --git a/src/Data/Parameterized/Classes.hs b/src/Data/Parameterized/Classes.hs
--- a/src/Data/Parameterized/Classes.hs
+++ b/src/Data/Parameterized/Classes.hs
@@ -8,6 +8,11 @@
 "Data.Functor.Classes" types as they work with any kind @k@, and are
 not restricted to '*'.
 -}
+
+-- TODO(#221): This is for the deprecation warning on
+-- Data.Parameterized.Compose, remove this when that module is removed.
+{-# OPTIONS_GHC -Wno-deprecations #-}
+
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DefaultSignatures #-}
@@ -65,14 +70,9 @@
 import Data.Maybe (isJust)
 import Data.Proxy
 import Data.Type.Equality as Equality
+import Lens.Micro (Lens', Traversal')
 
 import Data.Parameterized.Compose ()
-
--- We define these type alias here to avoid importing Control.Lens
--- modules, as this apparently causes problems with the safe Hasekll
--- checking.
-type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s
-type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s
 
 ------------------------------------------------------------------------
 -- CoercibleF
diff --git a/src/Data/Parameterized/Compose.hs b/src/Data/Parameterized/Compose.hs
--- a/src/Data/Parameterized/Compose.hs
+++ b/src/Data/Parameterized/Compose.hs
@@ -16,7 +16,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE Safe #-}
-module Data.Parameterized.Compose
+module Data.Parameterized.Compose {-# DEPRECATED "See #170" #-}
   ( testEqualityComposeBare
   ) where
 
@@ -37,3 +37,4 @@
   case (testEquality_ x y :: Maybe (g x :~: g y)) of
     Just Refl -> Just (Refl :: x :~: y)
     Nothing   -> Nothing
+{-# DEPRECATED testEqualityComposeBare "See #170" #-}
diff --git a/src/Data/Parameterized/Context.hs b/src/Data/Parameterized/Context.hs
--- a/src/Data/Parameterized/Context.hs
+++ b/src/Data/Parameterized/Context.hs
@@ -103,13 +103,14 @@
 import           Prelude hiding (unzip)
 
 import qualified Control.Applicative as App (liftA2)
-import           Control.Lens hiding (Index, (:>), Empty)
+import           Data.Function ((&))
 import           Data.Functor (void)
 import           Data.Functor.Product (Product(Pair))
 import           Data.Kind
 import qualified Data.Vector as V
 import qualified Data.Vector.Mutable as MV
 import           GHC.TypeLits (Nat, type (-))
+import           Lens.Micro (Lens', Lens, lens, (^.), (%~))
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
@@ -301,7 +302,7 @@
 --   ExtendBoth :: CtxEmbedding ctx ctx' -> CtxEmbedding (ctx ::> tp) (ctx' ::> tp)
 --   ExtendOne  :: CtxEmbedding ctx ctx' -> CtxEmbedding ctx (ctx' ::> tp)
 
-ctxeSize :: Simple Lens (CtxEmbedding ctx ctx') (Size ctx')
+ctxeSize :: Lens' (CtxEmbedding ctx ctx') (Size ctx')
 ctxeSize = lens _ctxeSize (\s v -> s { _ctxeSize = v })
 
 ctxeAssignment :: Lens (CtxEmbedding ctx1 ctx') (CtxEmbedding ctx2 ctx')
diff --git a/src/Data/Parameterized/Context/Safe.hs b/src/Data/Parameterized/Context/Safe.hs
--- a/src/Data/Parameterized/Context/Safe.hs
+++ b/src/Data/Parameterized/Context/Safe.hs
@@ -110,15 +110,15 @@
   ) where
 
 import qualified Control.Category as Cat
-import Control.DeepSeq
-import qualified Control.Lens as Lens
-import Control.Monad.Identity (Identity(..))
-import Data.Hashable
-import Data.List (intercalate)
-import Data.Maybe (listToMaybe)
-import Data.Type.Equality
-import Prelude hiding (init, map, null, replicate, succ, zipWith)
-import Data.Kind(Type)
+import           Control.DeepSeq
+import           Control.Monad.Identity (Identity(..))
+import           Data.Hashable
+import           Data.Kind (Type)
+import           Data.List (intercalate)
+import           Data.Maybe (listToMaybe)
+import           Data.Type.Equality
+import qualified Lens.Micro as Lens
+import           Prelude hiding (init, map, null, replicate, succ, zipWith)
 
 import Data.Parameterized.Classes
 import Data.Parameterized.Ctx
diff --git a/src/Data/Parameterized/Context/Unsafe.hs b/src/Data/Parameterized/Context/Unsafe.hs
--- a/src/Data/Parameterized/Context/Unsafe.hs
+++ b/src/Data/Parameterized/Context/Unsafe.hs
@@ -90,15 +90,15 @@
 import qualified Control.Category as Cat
 import           Control.DeepSeq
 import           Control.Exception
-import qualified Control.Lens as Lens
 import           Control.Monad.Identity (Identity(..))
 import           Data.Bits
 import           Data.Coerce
 import           Data.Hashable
+import           Data.Kind (Type)
 import           Data.List (intercalate)
 import           Data.Proxy
+import qualified Lens.Micro as Lens
 import           Unsafe.Coerce
-import           Data.Kind(Type)
 
 import           Data.Parameterized.Axiom
 import           Data.Parameterized.Classes
diff --git a/src/Data/Parameterized/Fin.hs b/src/Data/Parameterized/Fin.hs
--- a/src/Data/Parameterized/Fin.hs
+++ b/src/Data/Parameterized/Fin.hs
@@ -31,15 +31,11 @@
   , tryEmbed
   , minFin
   , incFin
-  , fin0Void
-  , fin1Unit
-  , fin2Bool
+  , fin0Absurd
   ) where
 
-import Control.Lens.Iso (Iso', iso)
 import GHC.TypeNats (KnownNat)
 import Numeric.Natural (Natural)
-import Data.Void (Void, absurd)
 
 import Data.Parameterized.NatRepr
 
@@ -124,25 +120,11 @@
   case leqAdd2 (LeqProof :: LeqProof (i + 1) n) (LeqProof :: LeqProof 1 1) of
     LeqProof -> mkFin (incNat i)
 
-fin0Void :: Iso' (Fin 0) Void
-fin0Void =
-  iso
-    (viewFin
-      (\(x :: NatRepr o) ->
-        case plusComm x (knownNat @1) of
-          Refl ->
-            case addIsLeqLeft1 @1 @o @0 LeqProof of {}))
-    absurd
-
-fin1Unit :: Iso' (Fin 1) ()
-fin1Unit = iso (const ()) (const minFin)
-
-fin2Bool :: Iso' (Fin 2) Bool
-fin2Bool =
-  iso
-    (viewFin
-      (\n ->
-         case isZeroNat n of
-           ZeroNat -> False
-           NonZeroNat -> True))
-    (\b -> if b then maxBound else minBound)
+-- | It is not possible to construct an element of @'Fin' 0@.
+fin0Absurd :: Fin 0 -> a
+fin0Absurd =
+  viewFin
+    (\(x :: NatRepr o) ->
+      case plusComm x (knownNat @1) of
+        Refl ->
+          case addIsLeqLeft1 @1 @o @0 LeqProof of {})
diff --git a/src/Data/Parameterized/List.hs b/src/Data/Parameterized/List.hs
--- a/src/Data/Parameterized/List.hs
+++ b/src/Data/Parameterized/List.hs
@@ -153,7 +153,7 @@
   , index3
   ) where
 
-import qualified Control.Lens as Lens
+import qualified Lens.Micro as Lens
 import           Data.Foldable
 import           Data.Kind
 import           Prelude hiding ((!!))
diff --git a/src/Data/Parameterized/Map.hs b/src/Data/Parameterized/Map.hs
--- a/src/Data/Parameterized/Map.hs
+++ b/src/Data/Parameterized/Map.hs
@@ -82,13 +82,13 @@
   ) where
 
 import           Control.Applicative hiding (empty)
-import           Control.Lens (Traversal', Lens')
 import           Control.Monad.Identity (Identity(..))
 import           Control.Monad (foldM)
 import           Data.Kind (Type)
 import qualified Data.List as List
 import           Data.Monoid
 import           Prelude hiding (filter, lookup, map, traverse, null)
+import           Lens.Micro (Traversal', Lens')
 
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
diff --git a/src/Data/Parameterized/Some.hs b/src/Data/Parameterized/Some.hs
--- a/src/Data/Parameterized/Some.hs
+++ b/src/Data/Parameterized/Some.hs
@@ -20,11 +20,11 @@
   , someLens
   ) where
 
-import Control.Lens (Lens', lens, (&), (^.), (.~))
 import Data.Hashable
-import Data.Kind
+import Data.Kind (Type)
 import Data.Parameterized.Classes
 import Data.Parameterized.TraversableF
+import Lens.Micro (Lens', lens, (&), (^.), (.~))
 
 
 data Some (f:: k -> Type) = forall x . Some (f x)
diff --git a/src/Data/Parameterized/TraversableFC/WithIndex.hs b/src/Data/Parameterized/TraversableFC/WithIndex.hs
--- a/src/Data/Parameterized/TraversableFC/WithIndex.hs
+++ b/src/Data/Parameterized/TraversableFC/WithIndex.hs
@@ -24,15 +24,21 @@
   , ifoldMapFCDefault
   ) where
 
+import Data.Coerce (Coercible, coerce)
 import Data.Functor.Const (Const(Const, getConst))
 import Data.Functor.Identity (Identity(Identity, runIdentity))
 import Data.Kind
 import Data.Monoid (All(..), Any(..), Endo(Endo), appEndo, Dual(Dual, getDual))
-import Data.Profunctor.Unsafe ((#.))
 import GHC.Exts (build)
 
 import Data.Parameterized.Classes
 import Data.Parameterized.TraversableFC
+
+-- See Note [Function coercion] in
+-- https://hackage-content.haskell.org/package/ghc-internal-9.1401.0/src/src/GHC/Internal/Data/Functor/Utils.hs
+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
+(#.) _f = coerce
+{-# INLINE (#.) #-}
 
 class FunctorFC t => FunctorFCWithIndex (t :: (k -> Type) -> l -> Type) where
   -- | Like 'fmapFC', but with an index.
diff --git a/test/Test/Context.hs b/test/Test/Context.hs
--- a/test/Test/Context.hs
+++ b/test/Test/Context.hs
@@ -18,7 +18,8 @@
   )
 where
 
-import           Control.Lens
+import           Data.Function ((&))
+import           Data.Functor.Identity (Identity(..))
 import           Data.Functor.Product (Product(Pair))
 import           Data.Kind
 import           Data.Parameterized.Classes
@@ -33,6 +34,7 @@
 import           Hedgehog
 import qualified Hedgehog.Gen as HG
 import           Hedgehog.Range
+import           Lens.Micro ((%~), (.~), over)
 import           Test.Tasty
 import           Test.Tasty.HUnit ( (@=?), (@?=), testCaseSteps )
 import           Test.Tasty.Hedgehog
diff --git a/test/Test/Some.hs b/test/Test/Some.hs
--- a/test/Test/Some.hs
+++ b/test/Test/Some.hs
@@ -7,7 +7,8 @@
 where
 
 import           Data.Type.Equality (TestEquality(testEquality), (:~:)(Refl))
-import           Control.Lens (Lens', lens, view, set)
+import           Lens.Micro (Lens', lens, set)
+import           Lens.Micro.Extras (view)
 
 import           Test.Tasty (TestTree, testGroup)
 import           Test.Tasty.HUnit (assertEqual, testCase)