diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,3 +10,8 @@
 
 * 0.1.0.1-4
   - minor fixes
+
+* 0.2.0.0
+  - added indexed codensity monad transformers
+  - rewrite of free indexed monad transformers
+  - doctests
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 BSD 3-Clause License
 
-Copyright (c) 2024, Morphism, LLC
+Copyright (c) 2026, Morphism, LLC
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,14 +1,18 @@
 # indexed-transformers
 
 An [Atkey indexed monad](https://bentnib.org/paramnotions-jfp.pdf)
-is a `Functor` [enriched category](https://ncatlab.org/nlab/show/enriched+category).
+is an endo`Functor` [enriched category](https://ncatlab.org/nlab/show/enriched+category),
+or [efect](https://mail.haskell.org/pipermail/haskell-cafe/2004-July/006448.html) for short.
 An indexed monad transformer transforms a `Monad` into an indexed monad.
 
 This library provides
   - a typeclass for indexed monad transformers
   - qualified do notation to use with them
+  - a typeclass for free indexed monad transformers
+  - a typeclass for state indexed monad transformers
   - and instances for the
-    - free indexed monad transformer
+    - free indexed monad transformers
+    - codensity indexed monad transformers
     - continuation indexed monad transformer
-    - state indexed monad transfomer
+    - state indexed monad transformer
     - writer indexed monad transformer
diff --git a/indexed-transformers.cabal b/indexed-transformers.cabal
--- a/indexed-transformers.cabal
+++ b/indexed-transformers.cabal
@@ -1,24 +1,25 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.36.0.
+-- This file has been generated from package.yaml by hpack version 0.39.6.
 --
 -- see: https://github.com/sol/hpack
 
 name:           indexed-transformers
-version:        0.1.0.4
+version:        0.2.0.0
 synopsis:       Atkey indexed monad transformers
 description:    Please see the README on GitHub at <https://github.com/morphismtech/indexed-transformers#readme>
 category:       Control
 homepage:       https://github.com/morphismtech/indexed-transformers#readme
 bug-reports:    https://github.com/morphismtech/indexed-transformers/issues
 author:         Eitan Chatav
-maintainer:     eitan@morphism.tech
-copyright:      2024 Eitan Chatav
+maintainer:     eitan.chatav@gmail.com
+copyright:      2026 Eitan Chatav
 license:        BSD-3-Clause
 license-file:   LICENSE
 build-type:     Simple
 extra-source-files:
     README.md
+extra-doc-files:
     CHANGELOG.md
 
 source-repository head
@@ -28,11 +29,10 @@
 library
   exposed-modules:
       Control.Monad.Trans.Indexed
+      Control.Monad.Trans.Indexed.Codensity
       Control.Monad.Trans.Indexed.Cont
       Control.Monad.Trans.Indexed.Do
       Control.Monad.Trans.Indexed.Free
-      Control.Monad.Trans.Indexed.Free.Fold
-      Control.Monad.Trans.Indexed.Free.Wrap
       Control.Monad.Trans.Indexed.State
       Control.Monad.Trans.Indexed.Writer
   other-modules:
@@ -44,20 +44,106 @@
   default-extensions:
       ConstraintKinds
       DeriveFunctor
+      DerivingStrategies
       FlexibleInstances
       GADTs
+      GeneralizedNewtypeDeriving
+      ImportQualifiedPost
       LambdaCase
       MultiParamTypeClasses
       PolyKinds
+      QualifiedDo
       QuantifiedConstraints
       RankNTypes
+      StandaloneDeriving
       StandaloneKindSignatures
       TupleSections
       TypeOperators
+      UndecidableInstances
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
   build-depends:
-      base >=4.7 && <5
-    , free
-    , mtl
-    , transformers
+      base >=4.18.1.0 && <5
+    , free >=5.2 && <6
+    , kan-extensions >=5.2.5 && <6
+    , mtl >=2.3.1 && <3
+    , transformers >=0.6.1.0 && <1
+  default-language: Haskell2010
+
+test-suite doctests
+  type: exitcode-stdio-1.0
+  main-is: Doctests.hs
+  other-modules:
+      Paths_indexed_transformers
+  autogen-modules:
+      Paths_indexed_transformers
+  hs-source-dirs:
+      test/doctests
+  default-extensions:
+      ConstraintKinds
+      DeriveFunctor
+      DerivingStrategies
+      FlexibleInstances
+      GADTs
+      GeneralizedNewtypeDeriving
+      ImportQualifiedPost
+      LambdaCase
+      MultiParamTypeClasses
+      PolyKinds
+      QualifiedDo
+      QuantifiedConstraints
+      RankNTypes
+      StandaloneDeriving
+      StandaloneKindSignatures
+      TupleSections
+      TypeOperators
+      UndecidableInstances
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded
+  build-depends:
+      base >=4.18.1.0 && <5
+    , doctest-parallel >=0.3.1 && <1
+    , free >=5.2 && <6
+    , indexed-transformers
+    , kan-extensions >=5.2.5 && <6
+    , mtl >=2.3.1 && <3
+    , transformers >=0.6.1.0 && <1
+  default-language: Haskell2010
+
+test-suite spec
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_indexed_transformers
+  autogen-modules:
+      Paths_indexed_transformers
+  hs-source-dirs:
+      test/spec
+  default-extensions:
+      ConstraintKinds
+      DeriveFunctor
+      DerivingStrategies
+      FlexibleInstances
+      GADTs
+      GeneralizedNewtypeDeriving
+      ImportQualifiedPost
+      LambdaCase
+      MultiParamTypeClasses
+      PolyKinds
+      QualifiedDo
+      QuantifiedConstraints
+      RankNTypes
+      StandaloneDeriving
+      StandaloneKindSignatures
+      TupleSections
+      TypeOperators
+      UndecidableInstances
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+  build-depends:
+      QuickCheck >=2.14.3 && <3
+    , base >=4.18.1.0 && <5
+    , free >=5.2 && <6
+    , hspec >=2.11.7 && <3
+    , indexed-transformers
+    , kan-extensions >=5.2.5 && <6
+    , mtl >=2.3.1 && <3
+    , transformers >=0.6.1.0 && <1
   default-language: Haskell2010
diff --git a/src/Control/Monad/Trans/Indexed.hs b/src/Control/Monad/Trans/Indexed.hs
--- a/src/Control/Monad/Trans/Indexed.hs
+++ b/src/Control/Monad/Trans/Indexed.hs
@@ -1,6 +1,6 @@
 {- |
 Module      :  Control.Monad.Trans.Indexed
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
@@ -48,7 +48,7 @@
   {- |
   indexed analog of `<*>`
 
-  prop> (<*>) = apIx
+  > prop> (<*>) = apIx
   -}
   apIx
     :: Monad m
@@ -60,8 +60,8 @@
   {- |
   indexed analog of `join`
 
-  prop> join = joinIx
-  prop> joinIx = bindIx id
+  > prop> join = joinIx
+  > prop> joinIx = bindIx id
   -}
   joinIx
     :: Monad m
@@ -72,10 +72,10 @@
   {- |
   indexed analog of `=<<`
 
-  prop> (=<<) = bindIx
-  prop> bindIx f x = joinIx (f <$> x)
-  prop> x & bindIx return = x
-  prop> x & bindIx f & bindIx g = x & bindIx (f & andThenIx g)
+  > prop> (=<<) = bindIx
+  > prop> bindIx f x = joinIx (f <$> x)
+  > prop> x & bindIx return = x
+  > prop> x & bindIx f & bindIx g = x & bindIx (f & andThenIx g)
   -}
   bindIx
     :: Monad m
@@ -87,8 +87,8 @@
   {- |
   indexed analog of flipped `>>`
 
-  prop> (>>) = flip thenIx
-  prop> return () & thenIx y = y
+  > prop> (>>) = flip thenIx
+  > prop> return () & thenIx y = y
   -}
   thenIx
     :: Monad m
@@ -100,11 +100,11 @@
   {- |
   indexed analog of `<=<`
 
-  prop> (<=<) = andThenIx
-  prop> andThenIx g f x = bindIx g (f x)
-  prop> f & andThenIx return = f
-  prop> return & andThenIx f = f
-  prop> f & andThenIx g & andThenIx h = f & andThenIx (g & andThenIx h)
+  > prop> (<=<) = andThenIx
+  > prop> andThenIx g f x = bindIx g (f x)
+  > prop> f & andThenIx return = f
+  > prop> return & andThenIx f = f
+  > prop> f & andThenIx g & andThenIx h = f & andThenIx (g & andThenIx h)
   -}
   andThenIx
     :: Monad m
diff --git a/src/Control/Monad/Trans/Indexed/Codensity.hs b/src/Control/Monad/Trans/Indexed/Codensity.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Indexed/Codensity.hs
@@ -0,0 +1,162 @@
+{- |
+Module      :  Control.Monad.Trans.Indexed.Codensity
+Copyright   :  (C) 2026 Eitan Chatav
+License     :  BSD 3-Clause License (see the file LICENSE)
+Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
+
+The indexed codensity monad transformer.
+-}
+
+module Control.Monad.Trans.Indexed.Codensity
+  ( CodensityIx (..)
+  , lowerCodensityIx
+  , liftCodensityIx
+  , toCodensity
+  , wrapCodensityIx
+  , resetCodensityIx
+  , shiftCodensityIx
+  , PredensityIx (..)
+  , lowerToStateIx
+  , liftFromStateIx
+  ) where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Codensity
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.State
+import Data.Kind
+
+{- |
+@'CodensityIx' t@ is the indexed monad transformer generated by taking
+the right Kan extension of any indexed monad transformer @t@ along itself.
+
+This can often be more \"efficient\" to construct than @t@ itself using
+repeated applications of 'bindIx',
+as in `Control.Monad.Trans.Indexed.Free.ImproveFreeIx`.
+
+See \"Asymptotic Improvement of Computations over Free Monads\" by Janis
+Voigtländer for more information.
+
+<https://www.janis-voigtlaender.eu/papers/AsymptoticImprovementOfComputationsOverFreeMonads.pdf>
+-}
+newtype CodensityIx t i j m a = CodensityIx
+  { runCodensityIx :: forall b k. (a -> t j k m b) -> t i k m b }
+  deriving Functor
+
+{- |
+This serves as the *left*-inverse (retraction) of 'liftCodensityIx'.
+
+> prop> lowerCodensityIx . liftCodensityIx ≡ id
+
+In general this is not a full 2-sided inverse, merely a retraction, as
+@'CodensityIx' t@ is often considerably \"larger\" than @t@.
+-}
+lowerCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => CodensityIx t i j m a -> t i j m a
+lowerCodensityIx (CodensityIx f) = f return
+
+{- | Lift a computation from the argument indexed monad
+to the constructed indexed monad. -}
+liftCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => t i j m a -> CodensityIx t i j m a
+liftCodensityIx m = CodensityIx $ \h -> bindIx h m
+
+{- | Convert to `Codensity`. -}
+toCodensity :: CodensityIx t i i m a -> Codensity (t i i m) a
+toCodensity (CodensityIx f) = Codensity f
+
+{- | Wrap the remainder of the 'CodensityIx' action
+using the given function. -}
+wrapCodensityIx
+  :: (forall a k. t j k (m :: Type -> Type) a -> t i k m a) -- ^ remainder
+  -> CodensityIx t i j m ()
+wrapCodensityIx f = CodensityIx (\k -> f (k ()))
+
+{- | @'resetCodensityIx' m@ delimits the continuation of any 'shiftCodensityIx' inside @m@.
+
+> prop> resetCodensityIx (return m) = return m
+-}
+resetCodensityIx :: (IxMonadTrans t, Monad m) => CodensityIx t i j m a -> CodensityIx t i j m a
+resetCodensityIx = liftCodensityIx . lowerCodensityIx
+
+{- | @'shiftCodensityIx' f@ captures the continuation up to the nearest enclosing
+'resetCodensityIx' and passes it to @f@:
+
+> prop> resetCodensityIx (shiftCodensityIx f & bindIx k) = resetCodensityIx (f (lowerCodensityIx . k))
+-}
+shiftCodensityIx
+  :: (IxMonadTrans t, Monad m)
+  => (forall b k. (a -> t j k m b) -> CodensityIx t i k m b)
+  -> CodensityIx t i j m a
+shiftCodensityIx f = CodensityIx $ lowerCodensityIx . f
+
+-- CodensityIx instances
+instance IxMonadTrans t => IxMonadTrans (CodensityIx t) where
+  joinIx (CodensityIx k) =
+    CodensityIx $ \f -> k $ \(CodensityIx g) -> g f
+instance i ~ j => Applicative (CodensityIx t i j m) where
+  pure x = CodensityIx $ \k -> k x
+  CodensityIx cf <*> CodensityIx cx =
+    CodensityIx $ \ k -> cf $ \ f -> cx (k . f)
+instance i ~ j => Monad (CodensityIx t i j m) where
+  return = pure
+  CodensityIx cx >>= k =
+    CodensityIx $ \ c -> cx (\ x -> runCodensityIx (k x) c)
+instance (IxMonadTrans t, i ~ j) => MonadTrans (CodensityIx t i j) where
+  lift m = CodensityIx (\k -> bindIx k (lift m))
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => Alternative (CodensityIx t i j m) where
+    empty = liftCodensityIx empty
+    x <|> y = liftCodensityIx (lowerCodensityIx x <|> lowerCodensityIx y)
+instance (i ~ j, Alternative (t i j m), IxMonadTrans t, Monad m)
+  => MonadPlus (CodensityIx t i j m)
+
+{- | `PredensityIx` `ReaderT` is an efficient encoding of `StateIx`.
+
+'lowerToStateIx' is the *left*-inverse (retraction) of 'liftFromStateIx'.
+
+> prop> lowerToStateIx . liftFromStateIx ≡ id
+
+In general this is not a full 2-sided inverse, merely a retraction, as
+@'PredensityIx' 'ReaderT'@ is \"larger\" than `StateIx`:
+it may call its continuation any number of times.
+-}
+newtype PredensityIx t i j m a = PredensityIx
+  { runPredensityIx :: forall b. (a -> t j m b) -> t i m b }
+  deriving Functor
+
+{- | Convert to `StateIx`. -}
+lowerToStateIx :: Monad m => PredensityIx ReaderT i j m a -> StateIx i j m a
+lowerToStateIx (PredensityIx f) =
+  StateIx . runReaderT . f $ \x -> ReaderT $ \j -> return (x, j)
+
+{- | Convert from `StateIx`. -}
+liftFromStateIx :: Monad m => StateIx i j m a -> PredensityIx ReaderT i j m a
+liftFromStateIx (StateIx f) =
+  PredensityIx $ \k -> ReaderT $ \i -> f i >>= \(x, j) -> runReaderT (k x) j
+
+-- PredensityIx instances
+instance (forall i. MonadTrans (t i)) => IxMonadTrans (PredensityIx t) where
+  joinIx (PredensityIx k) =
+    PredensityIx $ \f -> k $ \(PredensityIx g) -> g f
+instance i ~ j => Applicative (PredensityIx t i j m) where
+  pure x = PredensityIx $ \k -> k x
+  PredensityIx cf <*> PredensityIx cx =
+    PredensityIx $ \ k -> cf $ \ f -> cx (k . f)
+instance i ~ j => Monad (PredensityIx t i j m) where
+  return = pure
+  PredensityIx cx >>= k =
+    PredensityIx $ \ c -> cx (\ x -> runPredensityIx (k x) c)
+instance (MonadTrans (t i), i ~ j) => MonadTrans (PredensityIx t i j) where
+  lift m = PredensityIx (lift m >>=)
+instance (i ~ j, Monad m) => MonadState i (PredensityIx ReaderT i j m) where
+  get = getIx
+  put = putIx
+instance IxMonadTransState (PredensityIx ReaderT) where
+  getIx = PredensityIx (ask >>=)
+  putIx j = PredensityIx (\k -> withReaderT (const j) (k ()))
diff --git a/src/Control/Monad/Trans/Indexed/Cont.hs b/src/Control/Monad/Trans/Indexed/Cont.hs
--- a/src/Control/Monad/Trans/Indexed/Cont.hs
+++ b/src/Control/Monad/Trans/Indexed/Cont.hs
@@ -1,10 +1,14 @@
 {- |
 Module      :  Control.Monad.Trans.Indexed.Cont
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
 The continuation indexed monad transformer.
+
+Delimited continuation operators are taken from Kenichi Asai and Oleg
+Kiselyov's tutorial at CW 2011, [Introduction to programming with
+shift and reset](http://okmij.org/ftp/continuations/#tutorial).
 -}
 
 module Control.Monad.Trans.Indexed.Cont
@@ -23,6 +27,11 @@
 import Control.Monad.Trans
 import Control.Monad.Trans.Indexed
 
+{- | The continuation indexed monad transformer.
+Can be used to add continuation handling to any type constructor:
+the 'Monad' instance and most of the operations do not require @m@
+to be a monad.
+-}
 newtype ContIx i j m x = ContIx {runContIx :: (x -> m j) -> m i}
   deriving Functor
 instance IxMonadTrans ContIx where
@@ -37,26 +46,68 @@
   lift = ContIx . (>>=)
 instance i ~ j => MonadCont (ContIx i j m) where callCC = callCCIx
 
+{- | The result of running a CPS computation with 'return' as the
+final continuation.
+
+> prop> evalContIx (lift m) = m
+-}
 evalContIx :: Monad m => ContIx x j m j -> m x
 evalContIx c = runContIx c return
 
+{- | Apply a function to transform the result of a continuation-passing
+computation.
+
+> prop> runContIx (mapContIx f m) = f . runContIx m
+-}
 mapContIx :: (m i -> m j) -> ContIx i k m x -> ContIx j k m x
 mapContIx g (ContIx f) = ContIx $ g . f
 
+{- | Apply a function to transform the continuation passed to a CPS
+computation.
+
+> prop> runContIx (withContIx f m) = runContIx m . f
+-}
 withContIx :: ((y -> m k) -> x -> m j) -> ContIx i j m x -> ContIx i k m y
 withContIx f (ContIx g) = ContIx $ g . f
 
+{- | @callCCIx@ (call-with-current-continuation) calls its argument
+function, passing it the current continuation.  It provides
+an escape continuation mechanism for use with continuation
+monads.  Escape continuations allow one to abort the current
+computation and return a value immediately.  They achieve
+a similar effect to 'Control.Monad.Trans.Except.throwE'
+and 'Control.Monad.Trans.Except.catchE' within an
+'Control.Monad.Trans.Except.ExceptT' monad.  The advantage of this
+function over calling 'return' is that it makes the continuation
+explicit, allowing more flexibility and better control.
+
+The standard idiom used with @callCCIx@ is to provide a lambda-expression
+to name the continuation. Then calling the named continuation anywhere
+within its scope will escape from the computation, even if it is many
+layers deep within nested computations.
+-}
 callCCIx :: ((x -> ContIx j k m y) -> ContIx i j m x) -> ContIx i j m x
 callCCIx f = ContIx $ \k -> runContIx (f (ContIx . const . k)) k
 
+{- | @'shiftIx' f@ captures the continuation up to the nearest enclosing
+'resetIx' and passes it to @f@:
+
+> prop> resetIx (shiftIx f >>= k) = resetIx (f (evalContIx . k))
+-}
 shiftIx :: Monad m => ((x -> m j) -> ContIx i k m k) -> ContIx i j m x
 shiftIx f = ContIx (evalContIx . f)
 
+{- | @'resetIx' m@ delimits the continuation of any 'shiftIx' inside @m@.
+
+> prop> resetIx (lift m) = lift m
+-}
 resetIx :: Monad m => ContIx x j m j -> ContIx i i m x
 resetIx = lift . evalContIx
 
+{- | Convert to `ContT`. -}
 toContT :: ContIx i i m x -> ContT i m x
 toContT (ContIx f) = ContT f
 
+{- | Convert from `ContT`. -}
 fromContT :: ContT i m x -> ContIx i i m x
 fromContT (ContT f) = ContIx f
diff --git a/src/Control/Monad/Trans/Indexed/Do.hs b/src/Control/Monad/Trans/Indexed/Do.hs
--- a/src/Control/Monad/Trans/Indexed/Do.hs
+++ b/src/Control/Monad/Trans/Indexed/Do.hs
@@ -1,6 +1,6 @@
 {- |
 Module      :  Control.Monad.Trans.Indexed.Do
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
@@ -22,6 +22,7 @@
 import qualified Control.Monad.Trans.Indexed as Ix
 import Prelude hiding ((>>=), (>>), fail)
 
+{- | Indexed binding. -}
 (>>=)
   :: (Ix.IxMonadTrans t, M.Monad m)
   => t i j m x
@@ -29,6 +30,7 @@
   -> t i k m y
 (>>=) = flip Ix.bindIx
 
+{- | Indexed sequencing. -}
 (>>)
   :: (Ix.IxMonadTrans t, M.Monad m)
   => t i j m x
@@ -36,6 +38,7 @@
   -> t i k m y
 (>>) = flip Ix.thenIx
 
+{- | Indexed failing. -}
 fail
   :: (Ix.IxMonadTrans t, M.MonadFail m, i ~ j)
   => String
diff --git a/src/Control/Monad/Trans/Indexed/Free.hs b/src/Control/Monad/Trans/Indexed/Free.hs
--- a/src/Control/Monad/Trans/Indexed/Free.hs
+++ b/src/Control/Monad/Trans/Indexed/Free.hs
@@ -1,32 +1,17 @@
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
-
 {- |
 Module      :  Control.Monad.Trans.Indexed.Free
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
 The free indexed monad transformer.
--}
 
-module Control.Monad.Trans.Indexed.Free
-  ( IxMonadTransFree (liftFreeIx, hoistFreeIx, foldFreeIx), coerceFreeIx
-  , IxFunctor, IxMap (IxMap), liftFreerIx, hoistFreerIx, foldFreerIx
-  ) where
-
-import Control.Monad.Free
-import Control.Monad.Trans.Indexed
-import Data.Kind
+#example#
 
-{- |
-The free `IxMonadTrans` generated by an `IxFunctor`
-is characterized by the `IxMonadTransFree` class
-up to the isomorphism `coerceFreeIx`.
+== Example
 
-`IxMonadTransFree` and `IxMap`, the free `IxMonadTrans` and
-the free `IxFunctor`, can be combined as a "freer" `IxMonadTrans`
-and used as a DSL generated by primitive commands like this
+Free and freer indexed monad transformers can be used as
+a domain specific language generated by primitive commands like this
 [Conor McBride example]
 (https://stackoverflow.com/questions/28690448/what-is-indexed-monad).
 
@@ -44,25 +29,19 @@
 :}
 
 >>> :{
-insert
-  :: (IxMonadTransFree freeIx, Monad m)
-  => DVD -> freeIx (IxMap DVDCommand) 'False 'True m ()
+insert :: Monad m => DVD -> FreerIx FreeIx DVDCommand 'False 'True m ()
 insert dvd = liftFreerIx (Insert dvd)
 :}
 
 >>> :{
-eject
-  :: (IxMonadTransFree freeIx, Monad m)
-  => freeIx (IxMap DVDCommand) 'True 'False m DVD
+eject :: Monad m => FreerIx FreeIx DVDCommand 'True 'False m DVD
 eject = liftFreerIx Eject
 :}
 
 >>> :set -XQualifiedDo
 >>> import qualified Control.Monad.Trans.Indexed.Do as Indexed
 >>> :{
-swap
-  :: (IxMonadTransFree freeIx, Monad m)
-  => DVD -> freeIx (IxMap DVDCommand) 'True 'True m DVD
+swap :: Monad m => DVD -> FreerIx FreeIx DVDCommand 'True 'True m DVD
 swap dvd = Indexed.do
   dvd' <- eject
   insert dvd
@@ -71,71 +50,220 @@
 
 >>> import Control.Monad.Trans
 >>> :{
-printDVD :: IxMonadTransFree freeIx => freeIx (IxMap DVDCommand) 'True 'True IO ()
+printDVD :: FreerIx FreeIx DVDCommand 'True 'True IO ()
 printDVD = Indexed.do
   dvd <- eject
   insert dvd
   lift $ putStrLn dvd
 :}
+-}
 
+module Control.Monad.Trans.Indexed.Free
+  ( IxMonadTransFree (..)
+  , FreeIx (..)
+  , improveIx, coerceFreeIx
+  , FreerIx, liftFreerIx, hoistFreerIx, foldFreerIx
+  , CoyonedaIx (..)
+  , WrapFreeIx (..)
+  , FoldFreeIx (..)
+  , ImproveFreeIx (..)
+  ) where
+
+import Control.Monad
+import Control.Monad.Free
+import Control.Monad.Trans
+import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.Codensity
+
+{- |
+The free `IxMonadTrans` generated by an indexed `Functor`
+is characterized by the `IxMonadTransFree` class
+up to the isomorphism `coerceFreeIx`.
 -}
 class
-  ( forall f. IxFunctor f => IxMonadTrans (freeIx f)
-  , forall f m i j. (IxFunctor f, Monad m, i ~ j)
+  ( forall f. (forall k l. Functor (f k l)) => IxMonadTrans (freeIx f)
+  , forall f m i j. (forall k l. Functor (f k l), Monad m, i ~ j)
     => MonadFree (f i j) (freeIx f i j m)
   ) => IxMonadTransFree freeIx where
+  -- | lift a computation 
   liftFreeIx
-    :: (IxFunctor f, Monad m)
-    => f i j x
+    :: (forall k l. Functor (f k l), Monad m)
+    => f i j x -- ^ computation
     -> freeIx f i j m x
+  -- | hoist a transformation
   hoistFreeIx
-    :: (IxFunctor f, IxFunctor g, Monad m)
-    => (forall i j x. f i j x -> g i j x)
+    :: (forall k l. Functor (f k l), forall k l. Functor (g k l), Monad m)
+    => (forall k l a. f k l a -> g k l a) -- ^ transformation
     -> freeIx f i j m x -> freeIx g i j m x
+  -- | fold with a monadic transformation 
   foldFreeIx
-    :: (IxFunctor f, IxMonadTrans t, Monad m)
-    => (forall i j x. f i j x -> t i j m x)
+    :: (forall k l. Functor (f k l), IxMonadTrans t, Monad m)
+    => (forall k l a. f k l a -> t k l m a) -- ^ monadic transformation
     -> freeIx f i j m x -> t i j m x
 
 {- |
-prop> coerceFreeIx = foldFreeIx liftFreeIx
-prop> id = coerceFreeIx . coerceFreeIx
+> prop> coerceFreeIx = foldFreeIx liftFreeIx
+> prop> id = coerceFreeIx . coerceFreeIx
 -}
 coerceFreeIx
-  :: (IxMonadTransFree freeIx0, IxMonadTransFree freeIx1, IxFunctor f, Monad m)
-  => freeIx0 f i j m x -> freeIx1 f i j m x 
+  :: ( IxMonadTransFree freeIx0
+     , IxMonadTransFree freeIx1
+     , forall k l. Functor (f k l)
+     , Monad m
+     )
+  => freeIx0 f i j m x -- ^ from free
+  -> freeIx1 f i j m x -- ^ to free
 coerceFreeIx = foldFreeIx liftFreeIx
 
-type IxFunctor
-  :: (k -> k -> Type -> Type)
-  -> Constraint
-type IxFunctor f = forall i j. Functor (f i j)
+{- | Right associate all binds in a computation that generates an indexed free monad transformer.
 
+This can improve the asymptotic efficiency of the result, while preserving semantics.
+
+See \"Asymptotic Improvement of Computations over Free Monads\" by Janis
+Voigtländer for more information about this combinator.
+
+<https://www.janis-voigtlaender.eu/papers/AsymptoticImprovementOfComputationsOverFreeMonads.pdf>
+-}
+improveIx
+  :: (forall k l. Functor (f k l), Monad m)
+  => (forall freeIx. IxMonadTransFree freeIx => freeIx f i j m a) -- ^ improve this
+  -> FreeIx f i j m a
+improveIx m = lowerCodensityIx (runImproveFreeIx m)
+
 {- |
-`IxMap` is the free `IxFunctor`. It's a left Kan extension.
-Combining `IxMonadTransFree` with `IxMap` as demonstrated in the above example,
-gives the "freer" `IxMonadTrans`, modeled on this
-[Oleg Kiselyov explanation]
+Combining `IxMonadTransFree` with `CoyonedaIx` gives the "freer" `IxMonadTrans`,
+modeled on this [Oleg Kiselyov explanation]
 (https://okmij.org/ftp/Computation/free-monad.html#freer).
+See the [example]("Control.Monad.Trans.Indexed.Free#example").
 -}
-data IxMap f i j x where
-  IxMap :: (x -> y) -> f i j x -> IxMap f i j y
-instance Functor (IxMap f i j) where
-  fmap g (IxMap f x) = IxMap (g . f) x
+type FreerIx freeIx f = freeIx (CoyonedaIx f)
 
+{- | `CoyonedaIx` is the free indexed `Functor`. -}
+data CoyonedaIx f i j x where
+  CoyonedaIx :: (x -> y) -> f i j x -> CoyonedaIx f i j y
+instance Functor (CoyonedaIx f i j) where
+  fmap g (CoyonedaIx f x) = CoyonedaIx (g . f) x
+
+-- | Lift a computation to `FreerIx`.
 liftFreerIx
   :: (IxMonadTransFree freeIx, Monad m)
-  => f i j x -> freeIx (IxMap f) i j m x
-liftFreerIx x = liftFreeIx (IxMap id x)
+  => f i j x -- ^ computation
+  -> FreerIx freeIx f i j m x
+liftFreerIx x = liftFreeIx (CoyonedaIx id x)
 
+-- | Hoist a transformation to `FreerIx`
 hoistFreerIx
   :: (IxMonadTransFree freeIx, Monad m)
-  => (forall i j x. f i j x -> g i j x)
-  -> freeIx (IxMap f) i j m x -> freeIx (IxMap g) i j m x
-hoistFreerIx f = hoistFreeIx (\(IxMap g x) -> IxMap g (f x))
+  => (forall k l a. f k l a -> g k l a) -- ^ transformation
+  -> FreerIx freeIx f i j m x -> FreerIx freeIx g i j m x
+hoistFreerIx f = hoistFreeIx (\(CoyonedaIx g x) -> CoyonedaIx g (f x))
 
+-- | Fold with a monadic transformation over `FreerIx`.
 foldFreerIx
   :: (IxMonadTransFree freeIx, IxMonadTrans t, Monad m)
-  => (forall i j x. f i j x -> t i j m x)
-  -> freeIx (IxMap f) i j m x -> t i j m x
-foldFreerIx f x = foldFreeIx (\(IxMap g y) -> g <$> f y) x
+  => (forall k l a. f k l a -> t k l m a) -- ^ monadic transformation
+  -> FreerIx freeIx f i j m x -> t i j m x
+foldFreerIx f x = foldFreeIx (\(CoyonedaIx g y) -> g <$> f y) x
+
+-- | A helper type for `FreeIx`.
+data WrapFreeIx f i j m x where
+  Unwrap :: x -> WrapFreeIx f i i m x
+  Wrap :: f i j (FreeIx f j k m x) -> WrapFreeIx f i k m x
+instance (forall k l. Functor (f k l), Monad m)
+  => Functor (WrapFreeIx f i j m) where
+    fmap f = \case
+      Unwrap x -> Unwrap $ f x
+      Wrap fm -> Wrap $ fmap (fmap f) fm
+
+-- | The free indexed monad transformer.
+newtype FreeIx f i j m x = FreeIx {runFreeIx :: m (WrapFreeIx f i j m x)}
+instance (forall k l. Functor (f k l), Monad m)
+  => Functor (FreeIx f i j m) where
+    fmap f (FreeIx m) = FreeIx $ fmap (fmap f) m
+instance (forall k l. Functor (f k l), i ~ j, Monad m)
+  => Applicative (FreeIx f i j m) where
+    pure = FreeIx . pure . Unwrap
+    (<*>) = apIx
+instance (forall k l. Functor (f k l), i ~ j, Monad m)
+  => Monad (FreeIx f i j m) where
+    return = pure
+    (>>=) = flip bindIx
+instance (forall k l. Functor (f k l), i ~ j)
+  => MonadTrans (FreeIx f i j) where
+    lift = FreeIx . fmap Unwrap
+instance (forall k l. Functor (f k l)) => IxMonadTrans (FreeIx f) where
+  joinIx (FreeIx mm) = FreeIx $ mm >>= \case
+    Unwrap (FreeIx m) -> m
+    Wrap fm -> return $ Wrap $ fmap joinIx fm
+instance
+  ( forall k l. Functor (f k l)
+  , Monad m
+  , i ~ j
+  ) => MonadFree (f i j) (FreeIx f i j m) where
+    wrap = FreeIx . return . Wrap
+instance IxMonadTransFree FreeIx where
+  liftFreeIx = FreeIx . return . Wrap . fmap return
+  hoistFreeIx f (FreeIx m) = FreeIx (fmap hoist_f m)
+    where
+      hoist_f = \case
+        Unwrap x -> Unwrap x
+        Wrap y -> Wrap (f (fmap (hoistFreeIx f) y))
+  foldFreeIx f (FreeIx m) = bindIx foldMap_f (lift m)
+    where
+      foldMap_f = \case
+        Unwrap x -> return x
+        Wrap y -> bindIx (foldFreeIx f) (f y)
+
+-- | The free indexed monad transformer, encoded as its `foldFreeIx` function.
+newtype FoldFreeIx g i j m x = FoldFreeIx
+  {runFoldFreeIx :: forall t. (IxMonadTrans t, Monad m)
+    => (forall k l a. g k l a -> t k l m a) -> t i j m x}
+instance (forall k l. Functor (f k l), Monad m) => Functor (FoldFreeIx f i j m) where
+  fmap f (FoldFreeIx k) = FoldFreeIx $ \step -> fmap f (k step)
+instance (forall k l. Functor (f k l), i ~ j, Monad m)
+  => Applicative (FoldFreeIx f i j m) where
+    pure x = FoldFreeIx $ const $ pure x
+    (<*>) = apIx
+instance (forall k l. Functor (f k l), i ~ j, Monad m)
+  => Monad (FoldFreeIx f i j m) where
+    return = pure
+    (>>=) = flip bindIx
+instance (forall k l. Functor (f k l), i ~ j)
+  => MonadTrans (FoldFreeIx f i j) where
+    lift m = FoldFreeIx $ const $ lift m
+instance (forall k l. Functor (f k l))
+  => IxMonadTrans (FoldFreeIx f) where
+    joinIx (FoldFreeIx g) = FoldFreeIx $ \k -> bindIx (\(FoldFreeIx f) -> f k) (g k)
+instance
+  ( forall k l. Functor (f k l)
+  , Monad m
+  , i ~ j
+  ) => MonadFree (f i j) (FoldFreeIx f i j m) where
+    wrap = join . liftFreeIx
+instance IxMonadTransFree FoldFreeIx where
+  liftFreeIx m = FoldFreeIx $ \k -> k m
+  hoistFreeIx f (FoldFreeIx k) = FoldFreeIx $ \g -> k (g . f)
+  foldFreeIx f (FoldFreeIx k) = k f
+
+-- | A helper type for `improveIx`.
+newtype ImproveFreeIx f i j m a = ImproveFreeIx
+  { runImproveFreeIx :: CodensityIx (FreeIx f) i j m a }
+deriving newtype instance Functor (ImproveFreeIx f i j m)
+deriving newtype instance i ~ j => Applicative (ImproveFreeIx f i j m)
+deriving newtype instance i ~ j => Monad (ImproveFreeIx f i j m)
+deriving newtype instance (forall k l. Functor (f k l), i ~ j) => MonadTrans (ImproveFreeIx f i j)
+deriving newtype instance (forall k l. Functor (f k l)) => IxMonadTrans (ImproveFreeIx f)
+instance
+  ( forall k l. Functor (f k l)
+  , Monad m
+  , i ~ j
+  ) => MonadFree (f i j) (ImproveFreeIx f i j m) where
+    wrap t = ImproveFreeIx $ CodensityIx $ \h ->
+      joinIx (liftFreeIx (fmap (\p -> runCodensityIx (runImproveFreeIx p) h) t))
+instance IxMonadTransFree ImproveFreeIx where
+    liftFreeIx = ImproveFreeIx . liftCodensityIx . liftFreeIx
+    hoistFreeIx f
+      = ImproveFreeIx . liftCodensityIx
+      . hoistFreeIx f
+      . lowerCodensityIx . runImproveFreeIx
+    foldFreeIx f = foldFreeIx f . lowerCodensityIx . runImproveFreeIx
diff --git a/src/Control/Monad/Trans/Indexed/Free/Fold.hs b/src/Control/Monad/Trans/Indexed/Free/Fold.hs
deleted file mode 100644
--- a/src/Control/Monad/Trans/Indexed/Free/Fold.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
-
-{- |
-Module      :  Control.Monad.Trans.Indexed.Free.Fold
-Copyright   :  (C) 2024 Eitan Chatav
-License     :  BSD 3-Clause License (see the file LICENSE)
-Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
-
-An instance of the free indexed monad transformer encoded as `foldFreeIx`.
--}
-
-module Control.Monad.Trans.Indexed.Free.Fold
-  ( FreeIx (..)
-  ) where
-
-import Control.Monad
-import Control.Monad.Free
-import Control.Monad.Trans
-import Control.Monad.Trans.Indexed
-import Control.Monad.Trans.Indexed.Free
-
-{- |
-`FreeIx` is the free indexed monad transformer encoded as its `foldFreeIx`.
-
-prop> foldFreeIx f freeIx = runFreeIx freeIx f
--}
-newtype FreeIx g i j m x = FreeIx
-  {runFreeIx :: forall t. (IxMonadTrans t, Monad m)
-    => (forall i j x. g i j x -> t i j m x) -> t i j m x}
-instance (IxFunctor f, Monad m) => Functor (FreeIx f i j m) where
-  fmap f (FreeIx k) = FreeIx $ \step -> fmap f (k step)
-instance (IxFunctor f, i ~ j, Monad m)
-  => Applicative (FreeIx f i j m) where
-    pure x = FreeIx $ const $ pure x
-    (<*>) = apIx
-instance (IxFunctor f, i ~ j, Monad m)
-  => Monad (FreeIx f i j m) where
-    return = pure
-    (>>=) = flip bindIx
-instance (IxFunctor f, i ~ j)
-  => MonadTrans (FreeIx f i j) where
-    lift m = FreeIx $ const $ lift m
-instance IxFunctor f
-  => IxMonadTrans (FreeIx f) where
-    joinIx (FreeIx g) = FreeIx $ \k -> bindIx (\(FreeIx f) -> f k) (g k)
-instance
-  ( IxFunctor f
-  , Monad m
-  , i ~ j
-  ) => MonadFree (f i j) (FreeIx f i j m) where
-    wrap = join . liftFreeIx
-instance IxMonadTransFree FreeIx where
-  liftFreeIx m = FreeIx $ \k -> k m
-  hoistFreeIx f (FreeIx k) = FreeIx $ \g -> k (g . f)
-  foldFreeIx f (FreeIx k) = k f
diff --git a/src/Control/Monad/Trans/Indexed/Free/Wrap.hs b/src/Control/Monad/Trans/Indexed/Free/Wrap.hs
deleted file mode 100644
--- a/src/Control/Monad/Trans/Indexed/Free/Wrap.hs
+++ /dev/null
@@ -1,66 +0,0 @@
-{- |
-Module      :  Control.Monad.Trans.Indexed.Free.Wrap
-Copyright   :  (C) 2024 Eitan Chatav
-License     :  BSD 3-Clause License (see the file LICENSE)
-Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
-
-An instance of the free indexed monad transformer.
--}
-
-module Control.Monad.Trans.Indexed.Free.Wrap
-  ( FreeIx (..)
-  , WrapIx (..)
-  ) where
-
-import Control.Monad.Free
-import Control.Monad.Trans
-import Control.Monad.Trans.Indexed
-import Control.Monad.Trans.Indexed.Free
-
-data WrapIx f i j m x where
-  Unwrap :: x -> WrapIx f i i m x
-  Wrap :: f i j (FreeIx f j k m x) -> WrapIx f i k m x
-instance (IxFunctor f, Monad m)
-  => Functor (WrapIx f i j m) where
-    fmap f = \case
-      Unwrap x -> Unwrap $ f x
-      Wrap fm -> Wrap $ fmap (fmap f) fm
-
-newtype FreeIx f i j m x = FreeIx {runFreeIx :: m (WrapIx f i j m x)}
-instance (IxFunctor f, Monad m)
-  => Functor (FreeIx f i j m) where
-    fmap f (FreeIx m) = FreeIx $ fmap (fmap f) m
-instance (IxFunctor f, i ~ j, Monad m)
-  => Applicative (FreeIx f i j m) where
-    pure = FreeIx . pure . Unwrap
-    (<*>) = apIx
-instance (IxFunctor f, i ~ j, Monad m)
-  => Monad (FreeIx f i j m) where
-    return = pure
-    (>>=) = flip bindIx
-instance (IxFunctor f, i ~ j)
-  => MonadTrans (FreeIx f i j) where
-    lift = FreeIx . fmap Unwrap
-instance IxFunctor f
-  => IxMonadTrans (FreeIx f) where
-    joinIx (FreeIx mm) = FreeIx $ mm >>= \case
-      Unwrap (FreeIx m) -> m
-      Wrap fm -> return $ Wrap $ fmap joinIx fm
-instance
-  ( IxFunctor f
-  , Monad m
-  , i ~ j
-  ) => MonadFree (f i j) (FreeIx f i j m) where
-    wrap = FreeIx . return . Wrap
-instance IxMonadTransFree FreeIx where
-  liftFreeIx = FreeIx . return . Wrap . fmap return
-  hoistFreeIx f (FreeIx m) = FreeIx (fmap hoist_f m)
-    where
-      hoist_f = \case
-        Unwrap x -> Unwrap x
-        Wrap y -> Wrap (f (fmap (hoistFreeIx f) y))
-  foldFreeIx f (FreeIx m) = bindIx foldMap_f (lift m)
-    where
-      foldMap_f = \case
-        Unwrap x -> return x
-        Wrap y -> bindIx (foldFreeIx f) (f y)
diff --git a/src/Control/Monad/Trans/Indexed/State.hs b/src/Control/Monad/Trans/Indexed/State.hs
--- a/src/Control/Monad/Trans/Indexed/State.hs
+++ b/src/Control/Monad/Trans/Indexed/State.hs
@@ -1,6 +1,6 @@
 {- |
 Module      :  Control.Monad.Trans.Indexed.State
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
@@ -11,15 +11,32 @@
   ( StateIx (..)
   , evalStateIx
   , execStateIx
-  , modifyIx
-  , putIx
   , toStateT
   , fromStateT
+  , IxMonadTransState (..), modifyIx
   ) where
 
+import Control.Monad.Reader
 import Control.Monad.State
 import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.Do qualified as Indexed
 
+{- | An indexed state transformer monad parameterized by:
+
+  * @i@ - The initial state.
+
+  * @j@ - The final state.
+
+  * @m@ - The inner monad.
+
+The 'return' function leaves the state unchanged, while 'bindIx' uses
+the final state of the first computation as the initial state of
+the second.
+
+An efficient encoding of `StateIx`, up to the retraction
+`Control.Monad.Trans.Indexed.Codensity.lowerToStateIx`, is
+`Control.Monad.Trans.Indexed.Codensity.PredensityIx` `ReaderT`.
+-}
 newtype StateIx i j m x = StateIx { runStateIx :: i -> m (x, j)}
   deriving Functor
 instance IxMonadTrans StateIx where
@@ -37,20 +54,52 @@
 instance (i ~ j, Monad m) => MonadState i (StateIx i j m) where
   state f = StateIx (return . f)
 
+{- | Evaluate a state computation with the given initial state
+and return the final value, discarding the final state.
+-}
 evalStateIx :: Monad m => StateIx i j m x -> i -> m x
 evalStateIx m i = fst <$> runStateIx m i
 
+{- | Evaluate a state computation with the given initial state
+and return the final state, discarding the final value.
+-}
 execStateIx :: Monad m => StateIx i j m x -> i -> m j
 execStateIx m i = snd <$> runStateIx m i
 
-modifyIx :: Applicative m => (i -> j) -> StateIx i j m ()
-modifyIx f = StateIx $ \i -> pure ((), f i)
-
-putIx :: Applicative m => j -> StateIx i j m ()
-putIx j = modifyIx (\ _ -> j)
-
+{- | Convert to `StateT`. -}
 toStateT :: StateIx i i m x -> StateT i m x
 toStateT (StateIx f) = StateT f
 
+{- | Convert from `StateT`. -}
 fromStateT :: StateT i m x -> StateIx i i m x
 fromStateT (StateT f) = StateIx f
+
+{- | Minimal definition is either both of @getIx@ and @putIx@ or just @stateIx@ -}
+class
+  ( IxMonadTrans t
+  , forall i m. Monad m => MonadState i (t i i m)
+  ) => IxMonadTransState t where
+  {-# MINIMAL stateIx | getIx, putIx #-}
+  -- | Return the state from the internals of the monad.
+  getIx :: Monad m => t i i m i
+  getIx = stateIx (\i -> return (i,i))
+  -- | Replace the state inside the monad.
+  putIx :: Monad m => j -> t i j m ()
+  putIx i = stateIx (\_ -> return ((),i))
+  -- | Embed a state action into the monad.
+  stateIx :: Monad m => (i -> m (x,j)) -> t i j m x
+  stateIx f = Indexed.do
+    i <- getIx
+    ~(x, j) <- lift (f i)
+    putIx j
+    return x
+instance IxMonadTransState StateIx where
+  stateIx = StateIx
+
+{- | @'modifyIx' f@ is an action that updates the state to the result of
+applying @f@ to the current state.
+
+> prop> modifyIx f = getIx & bindIx (putIx . f)
+-}
+modifyIx :: (IxMonadTransState t, Monad m) => (i -> j) -> t i j m ()
+modifyIx f = stateIx (\i -> return ((), f i))
diff --git a/src/Control/Monad/Trans/Indexed/Writer.hs b/src/Control/Monad/Trans/Indexed/Writer.hs
--- a/src/Control/Monad/Trans/Indexed/Writer.hs
+++ b/src/Control/Monad/Trans/Indexed/Writer.hs
@@ -1,6 +1,6 @@
 {- |
 Module      :  Control.Monad.Trans.Indexed.Writer
-Copyright   :  (C) 2024 Eitan Chatav
+Copyright   :  (C) 2026 Eitan Chatav
 License     :  BSD 3-Clause License (see the file LICENSE)
 Maintainer  :  Eitan Chatav <eitan.chatav@gmail.com>
 
@@ -24,6 +24,15 @@
 import Control.Monad.Trans
 import Control.Monad.Trans.Indexed
 
+{- | An indexed writer monad parameterized by:
+
+  * @w@ - the output to accumulate.
+
+  * @m@ - The inner monad.
+
+The 'return' function produces the output 'id', while `bindIx`
+combines the outputs of the subcomputations using '>>>'.
+-}
 newtype WriterIx w i j m x = WriterIx {runWriterIx :: m (x, w i j)}
   deriving Functor
 
@@ -47,26 +56,35 @@
     x <- m
     return (x, id)
 
+{- | Extract the return value from a writer computation. -}
 evalWriterIx :: Monad m => WriterIx w i j m x -> m x
 evalWriterIx (WriterIx m) = fst <$> m
 
+{- | Extract the output from a writer computation. -}
 execWriterIx :: Monad m => WriterIx w i j m x -> m (w i j)
 execWriterIx (WriterIx m) = snd <$> m
 
+{- | Map both the return value and output of a computation using
+the given function. -}
 mapWriterIx
   :: (m (x, w i j) -> n (y, q i j))
   -> WriterIx w i j m x
   -> WriterIx q i j n y
 mapWriterIx f m = WriterIx $ f (runWriterIx m)
 
+{- | @'tellIx' w@ is an action that produces the output @w@. -}
 tellIx :: Monad m => w i j -> WriterIx w i j m ()
 tellIx w = WriterIx (return ((), w))
 
+{- | @'listenIx' m@ is an action that executes the action @m@ and adds its
+output to the value of the computation. -}
 listenIx :: Monad m => WriterIx w i j m x -> WriterIx w i j m (x, w i j)
 listenIx (WriterIx m) = WriterIx $ do
   (x, w) <- m
   return ((x, w),w)
 
+{- | @'listensIx' f m@ is an action that executes the action @m@ and adds
+the result of applying @f@ to the output to the value of the computation. -}
 listensIx
   :: Monad m
   => (w i j -> y)
@@ -76,6 +94,9 @@
   (x, w) <- m
   return ((x, f w), w)
 
+{- | @'passIx' m@ is an action that executes the action @m@, which returns
+a value and a function, and returns the value, applying the function
+to the output. -}
 passIx
   :: Monad m
   => WriterIx w i j m (x, w i j -> q i j)
@@ -84,6 +105,9 @@
   ((x, f), w) <- m
   return (x, f w)
 
+{- | @'censorIx' f m@ is an action that executes the action @m@ and
+applies the function @f@ to its output, leaving the return value
+unchanged. -}
 censorIx :: Monad m => (w i j -> w i j) -> WriterIx w i j m x -> WriterIx w i j m x
 censorIx f (WriterIx m) = WriterIx $ do
   (x, w) <- m
diff --git a/test/doctests/Doctests.hs b/test/doctests/Doctests.hs
new file mode 100644
--- /dev/null
+++ b/test/doctests/Doctests.hs
@@ -0,0 +1,7 @@
+module Main (main) where
+
+import System.Environment (getArgs)
+import Test.DocTest (mainFromCabal)
+
+main :: IO ()
+main = mainFromCabal "indexed-transformers" =<< getArgs
diff --git a/test/spec/Spec.hs b/test/spec/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/spec/Spec.hs
@@ -0,0 +1,338 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Main (main) where
+
+import Control.Category (Category, (>>>))
+import Control.Category qualified as Category
+import Control.Monad
+import Control.Monad.Codensity (lowerCodensity)
+import Control.Monad.Cont (runContT)
+import Control.Monad.Free (wrap)
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.Monad.Trans.Indexed
+import Control.Monad.Trans.Indexed.Codensity
+import Control.Monad.Trans.Indexed.Cont
+import Control.Monad.Trans.Indexed.Do qualified as Indexed
+import Control.Monad.Trans.Indexed.Free
+import Control.Monad.Trans.Indexed.State
+import Control.Monad.Trans.Indexed.Writer
+import Control.Monad.Writer (Writer, runWriter, tell)
+import Data.Foldable
+import Data.Kind
+import Data.Proxy
+import Test.Hspec
+import Test.QuickCheck
+
+type W = Writer [Int]
+
+w :: ([Int], x) -> W x
+w (xs, x) = tell xs >> return x
+
+data Prog
+  = Done Int
+  | Tell Int Prog
+  | Op Int
+  | Bind Prog (Fun Int Prog)
+  deriving Show
+
+instance Arbitrary Prog where
+  arbitrary = sized go
+    where
+      go 0 = oneof [Done <$> arbitrary, Op <$> arbitrary]
+      go n = oneof
+        [ Done <$> arbitrary
+        , Op <$> arbitrary
+        , Tell <$> arbitrary <*> go (n - 1)
+        , Bind <$> go (n `div` 2) <*> resize (n `div` 2) arbitrary
+        ]
+  shrink = \case
+    Done _ -> []
+    Op n -> [Done n]
+    Tell _ p -> [p]
+    Bind p f -> [p] ++ [Bind p' f | p' <- shrink p]
+
+interp :: IxMonadTrans t => (Int -> t Int Int W Int) -> Prog -> t Int Int W Int
+interp op = \case
+  Done n -> pure n
+  Tell n p -> thenIx (interp op p) (lift (tell [n]))
+  Op n -> op n
+  Bind p f -> bindIx (interp op . applyFun f) (interp op p)
+
+stateOp :: IxMonadTransState t => Int -> t Int Int W Int
+stateOp n = stateIx $ \s -> tell [s] >> return (s, s + n)
+
+observeState :: StateIx Int Int W Int -> Int -> [Int]
+observeState m s = let ((x, s'), xs) = runWriter (runStateIx m s) in xs ++ [x, s']
+
+type Cmd :: Type -> Type -> Type -> Type
+data Cmd i j x where
+  Cmd :: Int -> Cmd Int Int Int
+
+runCmd :: Cmd i j x -> StateIx i j W x
+runCmd (Cmd n) = stateOp n
+
+newtype Log i j = Log [Int]
+  deriving (Eq, Show)
+instance Category Log where
+  id = Log []
+  Log ys . Log xs = Log (xs ++ ys)
+
+data Subject = forall t. IxMonadTrans t
+  => Subject String (Int -> t Int Int W Int) (t Int Int W Int -> Int -> [Int])
+
+data FreeSubject = forall (freeIx :: (Type -> Type -> Type -> Type) -> Type -> Type -> (Type -> Type) -> Type -> Type).
+  IxMonadTransFree freeIx => FreeSubject String (Proxy freeIx)
+
+freeSubjects :: [FreeSubject]
+freeSubjects =
+  [ FreeSubject "FreeIx" (Proxy @FreeIx)
+  , FreeSubject "FoldFreeIx" (Proxy @FoldFreeIx)
+  , FreeSubject "ImproveFreeIx" (Proxy @ImproveFreeIx)
+  ]
+
+freeProg :: IxMonadTransFree freeIx => Prog -> FreerIx freeIx Cmd Int Int W Int
+freeProg = interp (liftFreerIx . Cmd)
+
+observeFree :: IxMonadTransFree freeIx => FreerIx freeIx Cmd Int Int W Int -> Int -> [Int]
+observeFree = observeState . foldFreerIx runCmd
+
+stateSubjects :: [Subject]
+stateSubjects =
+  [ Subject "StateIx" stateOp observeState
+  , Subject "PredensityIx ReaderT" stateOp (observeState . lowerToStateIx)
+  , Subject "CodensityIx StateIx"
+      (liftCodensityIx . stateOp) (observeState . lowerCodensityIx)
+  , Subject "CodensityIx FreeIx"
+      (liftCodensityIx . liftFreerIx . Cmd)
+      (observeFree @FreeIx . lowerCodensityIx)
+  ] ++
+  [ Subject name (liftFreerIx . Cmd) (observeFree @freeIx)
+  | FreeSubject name (_ :: Proxy freeIx) <- freeSubjects
+  ]
+
+otherSubjects :: [Subject]
+otherSubjects =
+  [ Subject "WriterIx"
+      (\n -> thenIx (pure (n + 1)) (tellIx (Log [n])))
+      (\m _ ->
+        let ((x, Log ys), xs) = runWriter (runWriterIx m)
+        in [length xs] ++ xs ++ ys ++ [x])
+  , Subject "ContIx"
+      (\n -> ContIx $ \k -> (+ n) <$> k n)
+      (\m s ->
+        let (x, xs) = runWriter (runContIx m (\y -> tell [y] >> return (2 * y + s)))
+        in xs ++ [x])
+  ]
+
+laws :: Subject -> Spec
+laws (Subject name op run) = describe name $ do
+  let
+    p = interp op
+    (m0 =~= m1) s = run m0 s === run m1 s
+  it "left identity" $ property $ \(x :: Int) (Fn f) ->
+    bindIx (p . f) (pure x) =~= p (f x)
+  it "right identity" $ property $ \m ->
+    bindIx pure (p m) =~= p m
+  it "associativity" $ property $ \m (Fn f) (Fn g) ->
+    bindIx (p . g) (bindIx (p . f) (p m))
+      =~= bindIx (andThenIx (p . g) (p . f)) (p m)
+  it "joinIx" $ property $ \m (Fn f) ->
+    joinIx (p . f <$> p m) =~= bindIx (p . f) (p m)
+  it "(>>=) = flip bindIx" $ property $ \m (Fn f) ->
+    (p m >>= p . f) =~= bindIx (p . f) (p m)
+  it "(<*>) = apIx" $ property $ \m0 m1 (Fn2 f) ->
+    (f <$> p m0 <*> p m1) =~= apIx (f <$> p m0) (p m1)
+  it "(>>) = flip thenIx" $ property $ \m0 m1 ->
+    (p m0 >> p m1) =~= thenIx (p m1) (p m0)
+  it "fmap" $ property $ \m (Fn (f :: Int -> Int)) ->
+    (f <$> p m) =~= bindIx (pure . f) (p m)
+  it "lift . return = return" $ property $ \(x :: Int) ->
+    lift (return x) =~= pure x
+  it "lift (m >>= f) = lift m >>= lift . f" $ property $ \(m :: ([Int], Int)) (Fn (f :: Int -> ([Int], Int))) ->
+    lift (w m >>= w . f) =~= (lift (w m) >>= lift . w . f)
+
+stateLaws
+  :: forall t. IxMonadTransState t
+  => String
+  -> (forall i j x. t i j W x -> StateIx i j W x)
+  -> Spec
+stateLaws name toState = describe name $ do
+  let
+    run :: t i j W x -> i -> ((x, j), [Int])
+    run m s = runWriter (runStateIx (toState m) s)
+  it "getIx" $ property $ \(s :: Int) ->
+    run getIx s === ((s, s), [])
+  it "putIx" $ property $ \(s :: Int) (s' :: String) ->
+    run (putIx s') s === (((), s'), [])
+  it "stateIx" $ property $ \(Fn (f :: Int -> ([Int], (Bool, String)))) s ->
+    run (stateIx (w . f)) s === runWriter (w (f s))
+  it "modifyIx" $ property $ \(Fn (f :: Int -> String)) s ->
+    run (modifyIx f) s === (((), f s), [])
+  it "get then put" $ property $ \(s :: Int) ->
+    run (bindIx putIx getIx) s === run (pure ()) s
+  it "put then get" $ property $ \(s :: Int) (s' :: String) ->
+    run (thenIx getIx (putIx s')) s === run (thenIx (pure s') (putIx s')) s
+  it "put then put" $ property $ \(s :: Int) (s' :: Bool) (s'' :: String) ->
+    run (thenIx (putIx s'') (putIx s')) s === run (putIx s'') s
+  it "MonadState" $ property $ \(Fn (f :: Int -> Int)) s ->
+    run (state (\x -> (x, f x))) s === ((s, f s), [])
+  it "Indexed.do" $ property $ \(s :: Int) (s' :: String) ->
+    run
+      ( Indexed.do
+          putIx s'
+          x <- getIx
+          putIx (length x)
+          return x
+      ) s
+      === ((s', length s'), [])
+
+predensitySpec :: Spec
+predensitySpec = describe "PredensityIx ReaderT" $ do
+  it "lowerToStateIx . liftFromStateIx = id" $ property $
+    \(Fn (f :: Int -> ([Int], (Bool, String)))) s ->
+      let m = StateIx (w . f)
+      in runWriter (runStateIx (lowerToStateIx (liftFromStateIx m)) s)
+        === runWriter (runStateIx m s)
+  it "liftFromStateIx . lowerToStateIx = id on stateIx terms" $ property $
+    \prog (Fn2 (k :: Int -> Int -> ([Int], Int))) s ->
+      let
+        m = interp stateOp prog
+        run m' = runWriter (runReaderT (runPredensityIx m' (\x -> ReaderT (w . k x))) s)
+      in run (liftFromStateIx (lowerToStateIx m)) === run m
+
+codensitySpec :: Spec
+codensitySpec = describe "CodensityIx StateIx" $ do
+  let p = interp (liftCodensityIx . stateOp)
+  it "lowerCodensityIx . liftCodensityIx = id" $ property $ \prog s ->
+    let m = interp stateOp prog
+    in observeState (lowerCodensityIx (liftCodensityIx m)) s === observeState m s
+  it "resetCodensityIx" $ property $ \prog s ->
+    observeState (lowerCodensityIx (resetCodensityIx (p prog))) s
+      === observeState (lowerCodensityIx (p prog)) s
+  it "toCodensity" $ property $ \prog s ->
+    observeState (lowerCodensity (toCodensity (p prog))) s
+      === observeState (lowerCodensityIx (p prog)) s
+  it "wrapCodensityIx" $ property $ \(s :: Int) (s' :: String) ->
+    let m0 = lowerCodensityIx (wrapCodensityIx (\m -> thenIx m (putIx s'))) :: StateIx Int String W ()
+    in runWriter (runStateIx m0 s) === runWriter (runStateIx (putIx s') s)
+  it "shiftCodensityIx" $ property $ \(x :: Int) (n :: Int) (Fn f) s ->
+    observeState
+      (lowerCodensityIx
+        (shiftCodensityIx (\k -> liftCodensityIx (thenIx (k x) (modifyIx (+ n)))) >>= p . f))
+      s
+      === observeState (thenIx (lowerCodensityIx (p (f x))) (modifyIx (+ n))) s
+
+freeSpec :: FreeSubject -> Spec
+freeSpec (FreeSubject name (_ :: Proxy freeIx)) = describe name $ do
+  forM_ freeSubjects $ \(FreeSubject name' (_ :: Proxy freeIx')) ->
+    it ("coerceFreeIx to " <> name') $ property $ \prog s ->
+      observeFree @freeIx' (coerceFreeIx (freeProg @freeIx prog)) s
+        === observeFree @freeIx (freeProg prog) s
+  it "foldFreeIx f . liftFreeIx = f" $ property $ \n s ->
+    observeFree @freeIx (liftFreerIx (Cmd n)) s === observeState (runCmd (Cmd n)) s
+  it "hoistFreerIx" $ property $ \prog s ->
+    let double :: Cmd i j x -> Cmd i j x
+        double (Cmd n) = Cmd (2 * n)
+    in observeFree (hoistFreerIx double (freeProg @freeIx prog)) s
+      === observeState (foldFreerIx (runCmd . double) (freeProg @freeIx prog)) s
+  it "wrap" $ property $ \n (Fn f) s ->
+    observeFree @freeIx (wrap (CoyonedaIx (freeProg . f) (Cmd n))) s
+      === observeFree @freeIx (bindIx (freeProg . f) (liftFreerIx (Cmd n))) s
+  it "improveIx" $ property $ \prog s ->
+    observeFree (improveIx (freeProg prog)) s === observeFree @freeIx (freeProg prog) s
+
+contSpec :: Spec
+contSpec = describe "ContIx" $ do
+  let
+    p :: Prog -> ContIx Int Int W Int
+    p = interp (\n -> ContIx $ \k -> (+ n) <$> k n)
+    eval = runWriter . evalContIx
+  it "callCCIx" $ property $ \prog (x :: Int) ->
+    eval (callCCIx (\k -> thenIx (p prog) (k x))) === eval (pure x)
+  it "shiftIx" $ property $ \(x :: Int) (Fn g) ->
+    eval (g <$> shiftIx (\k -> lift (k x >>= k))) === eval (pure (g (g x)))
+  it "resetIx" $ property $ \prog ->
+    eval (resetIx (p prog) :: ContIx Int Int W Int) === eval (p prog)
+  it "withContIx" $ property $ \prog (Fn (f :: Int -> Int)) ->
+    eval (withContIx (\k -> k . f) (p prog)) === eval (f <$> p prog)
+  it "toContT . fromContT" $ property $ \prog ->
+    runWriter (runContT (toContT (fromContT (toContT (p prog)))) return)
+      === eval (p prog)
+
+writerSpec :: Spec
+writerSpec = describe "WriterIx" $ do
+  let
+    run :: WriterIx Log i j W x -> ((x, Log i j), [Int])
+    run = runWriter . runWriterIx
+  it "tellIx" $ property $ \xs ys ->
+    run (thenIx (tellIx (Log ys)) (tellIx (Log xs)) :: WriterIx Log Int Bool W ())
+      === run (tellIx (Log xs >>> Log ys))
+  it "listenIx" $ property $ \xs (x :: Int) ->
+    let m = thenIx (pure x) (tellIx (Log xs)) :: WriterIx Log Int Bool W Int
+    in run (listenIx m) === (((x, Log xs), Log xs), [])
+  it "listensIx" $ property $ \xs (x :: Int) ->
+    let m = thenIx (pure x) (tellIx (Log xs)) :: WriterIx Log Int Bool W Int
+    in run (listensIx (\(Log ys) -> sum ys) m) === (((x, sum xs), Log xs), [])
+  it "censorIx" $ property $ \xs (Fn f) ->
+    run (censorIx (\(Log ys) -> Log (f ys)) (tellIx (Log xs) :: WriterIx Log Int Bool W ()))
+      === (((), Log (f xs)), [])
+  it "passIx" $ property $ \xs (Fn f) (x :: Int) ->
+    run (passIx (WriterIx (return ((x, \(Log ys) -> Log (f ys)), Log xs))) :: WriterIx Log Int Bool W Int)
+      === ((x, Log (f xs)), [])
+  it "evalWriterIx and execWriterIx" $ property $ \xs (x :: Int) ->
+    let m = thenIx (pure x) (tellIx (Log xs)) :: WriterIx Log Int Bool W Int
+    in (runWriter (evalWriterIx m), runWriter (execWriterIx m)) === ((x, []), (Log xs, []))
+
+categorySpec :: Spec
+categorySpec = describe "Indexed StateIx" $ do
+  let
+    st :: Fun i ([Int], ([Int], j)) -> Indexed StateIx W [Int] i j
+    st (Fn f) = Indexed (StateIx (w . f))
+    run :: Indexed StateIx W [Int] i j -> i -> (([Int], j), [Int])
+    run m s = runWriter (runStateIx (runIndexed m) s)
+  it "left identity" $ property $ \(f :: Fun Int ([Int], ([Int], String))) s ->
+    run (Category.id Category.. st f) s === run (st f) s
+  it "right identity" $ property $ \(f :: Fun Int ([Int], ([Int], String))) s ->
+    run (st f Category.. Category.id) s === run (st f) s
+  it "associativity" $ property $
+    \(f :: Fun Int ([Int], ([Int], String)))
+     (g :: Fun String ([Int], ([Int], Bool)))
+     (h :: Fun Bool ([Int], ([Int], Int)))
+     s ->
+      run ((st h Category.. st g) Category.. st f) s
+        === run (st h Category.. (st g Category.. st f)) s
+
+stateSpec :: Spec
+stateSpec = describe "StateIx" $ do
+  it "toStateT" $ property $ \prog s ->
+    let m = interp stateOp prog
+    in runWriter (runStateT (toStateT m) s) === runWriter (runStateIx m s)
+  it "fromStateT . toStateT = id" $ property $ \prog s ->
+    let m = interp stateOp prog
+    in observeState (fromStateT (toStateT m)) s === observeState m s
+  it "evalStateIx and execStateIx" $ property $ \prog s ->
+    let m = interp stateOp prog
+        ((x, s'), xs) = runWriter (runStateIx m s)
+    in (runWriter (evalStateIx m s), runWriter (execStateIx m s)) === ((x, xs), (s', xs))
+
+main :: IO ()
+main = hspec $ do
+  describe "IxMonadTrans laws" $
+    mapM_ laws (stateSubjects ++ otherSubjects)
+  describe "state transformers agree with StateIx" $
+    forM_ stateSubjects $ \(Subject name op run) ->
+      it name $ property $ \prog s ->
+        run (interp op prog) s === observeState (interp stateOp prog) s
+  describe "IxMonadTransState laws" $ do
+    stateLaws "StateIx" id
+    stateLaws "PredensityIx ReaderT" lowerToStateIx
+  predensitySpec
+  codensitySpec
+  describe "IxMonadTransFree" $ traverse_ freeSpec freeSubjects
+  contSpec
+  writerSpec
+  categorySpec
+  stateSpec