diff --git a/debruijn-safe.cabal b/debruijn-safe.cabal
--- a/debruijn-safe.cabal
+++ b/debruijn-safe.cabal
@@ -1,6 +1,6 @@
 cabal-version: 2.4
 name:          debruijn-safe
-version:       0.3
+version:       0.3.1
 license:       BSD-3-Clause
 license-file:  LICENSE
 category:      Development
@@ -13,7 +13,13 @@
 author:        Oleg Grenrus <oleg.grenrus@iki.fi>
 maintainer:    Oleg Grenrus <oleg.grenrus@iki.fi>
 build-type:    Simple
-tested-with:   GHC ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.2 || ==9.10.1
+tested-with:
+  GHC ==9.2.8
+   || ==9.4.8
+   || ==9.6.7
+   || ==9.8.4
+   || ==9.10.2
+   || ==9.12.2
 
 source-repository head
   type:     git
@@ -27,7 +33,7 @@
 
   -- GHC-boot libraries
   build-depends:
-    , base     ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 || ^>=4.20.0.0
+    , base     ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0 || ^>=4.20.0.0 || ^>=4.21.0.0
     , deepseq  ^>=1.4.6.1  || ^>=1.5.0.0
 
   -- rest of the dependencies
diff --git a/src/DeBruijn/Env.hs b/src/DeBruijn/Env.hs
--- a/src/DeBruijn/Env.hs
+++ b/src/DeBruijn/Env.hs
@@ -4,6 +4,7 @@
     lookupEnv,
     sizeEnv,
     tabulateEnv,
+    zipWithEnv,
 ) where
 
 import Data.Kind (Type)
@@ -72,7 +73,7 @@
 -- 'b'
 --
 lookupEnv :: Idx ctx -> Env ctx a -> a
-lookupEnv IZ     (_  :> x)  = x
+lookupEnv IZ     (_  :> x) = x
 lookupEnv (IS n) (xs :> _) = lookupEnv n xs
 
 -- | Size of the environment.
@@ -87,3 +88,13 @@
 tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a
 tabulateEnv SZ     _ = EmptyEnv
 tabulateEnv (SS s) f = tabulateEnv s (f . IS) :> f IZ
+
+-- |
+--
+-- >>> zipWithEnv (,) (EmptyEnv :> 'a') (EmptyEnv :> True)
+-- EmptyEnv :> ('a',True)
+--
+-- @since 0.3.1
+zipWithEnv :: (a -> b -> c) -> Env ctx a -> Env ctx b -> Env ctx c
+zipWithEnv _ EmptyEnv  EmptyEnv  = EmptyEnv
+zipWithEnv f (xs :> x) (ys :> y) = zipWithEnv f xs ys :> f x y
diff --git a/src/DeBruijn/Idx.hs b/src/DeBruijn/Idx.hs
--- a/src/DeBruijn/Idx.hs
+++ b/src/DeBruijn/Idx.hs
@@ -33,16 +33,16 @@
 type Idx :: Ctx -> Type
 type role Idx nominal
 
-data Idx n where
-    IZ :: Idx (S n)
-    IS :: !(Idx n) -> Idx (S n)
+data Idx ctx where
+    IZ :: Idx (S ctx)
+    IS :: !(Idx ctx) -> Idx (S ctx)
 
 -------------------------------------------------------------------------------
 -- Combinators
 -------------------------------------------------------------------------------
 
 -- | Convert index to 'Int'.
-idxToInt :: Idx n -> Int
+idxToInt :: Idx ctx -> Int
 idxToInt = go 0 where
     go :: Int -> Idx j -> Int
     go !acc IZ = acc
@@ -58,8 +58,8 @@
 -- Instances
 -------------------------------------------------------------------------------
 
-deriving instance Eq (Idx n)
-deriving instance Ord (Idx n)
+deriving instance Eq (Idx ctx)
+deriving instance Ord (Idx ctx)
 
 instance Show (Idx j) where
     showsPrec d = showsPrec d . idxToInt
diff --git a/src/DeBruijn/Lvl.hs b/src/DeBruijn/Lvl.hs
--- a/src/DeBruijn/Lvl.hs
+++ b/src/DeBruijn/Lvl.hs
@@ -3,13 +3,14 @@
     Lvl,
     lvlToIdx,
     lvlZ,
-    sinkLvl,
+    idxToLvl,
+    -- * Sinking
     Sinkable (..),
     sink,
-    mapSink,
     sinkSize,
-    mapSinkSize,
     sinkAdd,
+    mapSink,
+    mapSinkSize,
     mapSinkAdd,
 ) where
 
@@ -58,6 +59,14 @@
 lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
 lvlToIdx _ (MkLvl _ x) = x
 
+-- | Convert index to level.
+--
+-- >>> idxToLvl S2 (IS IZ)
+-- 1
+--
+idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
+idxToLvl s x = (MkLvl (sizeToInt s - idxToInt x) x)
+
 -- | Last level.
 --
 -- >>> lvlZ S1
@@ -69,6 +78,7 @@
 lvlZ :: Size ctx -> Lvl (S ctx)
 lvlZ s = MkLvl (sizeToInt s) IZ
 
+{- TODO?
 -- | Sink 'Lvl' into a larger context.
 --
 -- >>> sinkLvl (lvlZ S3)
@@ -83,6 +93,7 @@
 --
 sinkLvl :: Lvl ctx -> Lvl (S ctx)
 sinkLvl (MkLvl s i) = MkLvl s (IS i)
+-}
 
 -------------------------------------------------------------------------------
 -- Sinkable