diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,16 @@
 # Revision history for functor-monad
 
+## 0.1.1.1 -- 2024-09-29
+
+* Add a module `TrailAsAdjunction` to the examples directory,
+  just as an explanation of theoretical background.
+
+* Fix some documentation errors
+
+## 0.1.1.0 -- 2024-02-07
+
+* The first published version
+
 ## 0.1.0.0 (review) -- 2023-12-23
 
 * First version
diff --git a/examples/TrailAsAdjunction.hs b/examples/TrailAsAdjunction.hs
new file mode 100644
--- /dev/null
+++ b/examples/TrailAsAdjunction.hs
@@ -0,0 +1,241 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE TupleSections #-}
+
+-- | Explain 'Control.Monad.Trail.Trail' monad in terms of adjoint functors
+module TrailAsAdjunction(
+  -- * Building blocks
+
+  Const(..), Pair, Shape(..), Emptied(..), Y, Γ(..),
+
+  mapPair, mapShape, mapEmptied, mapY, mapΓ,
+
+  -- * Adjunctions
+  -- $adjunction_diagrams
+
+  adjunctPairShape,
+  adjunctPairShape',
+  adjunctShapeConst,
+  adjunctShapeConst',
+  adjunctConstEmptied,
+  adjunctConstEmptied',
+  adjunctΓY,
+  adjunctΓY',
+
+  -- * Monads and Comonads from these adjunctions
+
+  J0(..), K1(..), J1(..), RR(..),
+
+  -- * Examples
+  --
+  -- $doc_example
+
+  R(..),
+
+) where
+
+import Data.Void
+import Data.Bifunctor (Bifunctor(..))
+import Data.Functor.Const
+import Control.Comonad
+import Control.Monad (ap)
+import Data.Coerce (coerce)
+
+import FFunctor (FFunctor(..), type (~>))
+import FMonad (FMonad (..))
+import FComonad (FComonad (..))
+
+
+{- $adjunction_diagrams
+
+There is a chain of three adjunctions between @Type@ and @Functor@
+
+>                    Type
+>   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+>      |            ^          |            ^
+>      |            |          |            |
+> Pair |  -|  Shape | -| Const | -| Emptied | 
+>      |            |          |            |
+>      v            |          v            |
+>   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+>                   Functor
+
+And an adjunction between @Type^op@ and @Functor@
+
+>       Type^op
+>   ~~~~~~~~~~~~~~~~
+>      ^      |
+>      |      |
+>    Γ |  -|  | Y
+>      |      |
+>      |      v
+>   ~~~~~~~~~~~~~~~~
+>      Functor
+
+-}
+
+{- $doc_example
+
+'J0' and 'J1' turn an @FMonad mm@ to a @Monad@. The following table shows what is the
+@Monad@ they make for each @FMonad@.
+
++-----------+-------------+--------------------+-------------------+------------+------------+
+| @mm@      | @Compose m@ | @Precompose m@     | @Sum f@           | @Free@     | @FreeT' m@ |
++===========+=============+====================+===================+============+============+
+| @'J0' mm@ | @m@         | @Identity@         | @Either (f Void)@ | @Identity@ | @m@        |
++-----------+-------------+--------------------+-------------------+------------+------------+
+| @'J1' mm@ | @m@         | @Writer (Ap m ())@ | @Either (f ())@   | @[]@       | @ListT m@  |
++-----------+-------------+--------------------+-------------------+------------+------------+
+
+'K1' takes an @FComonad ww@ and turns them a @Comonad@. 'RR' takes an @FComonad ww@ and turns
+them a @Monad@, instead of @Comonad@.
+
++-----------+-------------+--------------------+-------------------+------------+---------------------+
+| @ww@      | @Compose w@ | @Precompose w@     | @Product f@       | @Cofree@   | @Sum ff gg@         |
++===========+=============+====================+===================+============+=====================+
+| @'K1' ww@ | @w@         | @Identity@         | @Env (f ())@      | @Identity@ | @K1 ff :+: K1 gg@   |
++-----------+-------------+--------------------+-------------------+------------+---------------------+
+| @'RR' ww@ | @Co w@      | @R w@              | @Exp1 f Identity@ | @[]@       | ??                  |
++-----------+-------------+--------------------+-------------------+------------+---------------------+
+
+Where
+
+- 'Control.Monad.Co.Co' is a @Monad@ defined in "Control.Monad.Co" from kan-extensions package
+- 'R' is a @Monad@ defined below
+- 'Data.Functor.Exp.Exp1' is defined in "Data.Functor.Exp"
+
+-}
+
+-- * Building blocks
+
+-- | @Pair :: Type -> Functor@
+type Pair = (,)
+
+mapPair :: (a -> b) -> (Pair a ~> Pair b)
+mapPair = first
+
+-- | Yoneda embedding
+--
+-- @Y :: Type^op -> Functor@
+type Y = (->)
+
+mapY :: (a -> b) -> (Y b ~> Y a)
+mapY = flip (.)
+
+-- | @Emptied :: Functor -> Type@
+newtype Emptied f = Emptied { getEmptied :: f Void }
+
+mapEmptied :: (f ~> g) -> Emptied f -> Emptied g
+mapEmptied fg (Emptied f0) = Emptied (fg f0)
+
+-- | @Shape :: Functor -> Type@
+newtype Shape f = Shape { getShape :: f () }
+
+mapShape :: (f ~> g) -> Shape f -> Shape g
+mapShape fg (Shape f1) = Shape (fg f1)
+
+-- | @Γ :: Functor -> Type^op@
+newtype Γ f = Γ { getΓ :: forall x. f x -> x }
+
+mapΓ :: (f ~> g) -> Γ g -> Γ f
+mapΓ fg (Γ k) = Γ (k . fg)
+
+-- * Adjunctions
+
+adjunctPairShape :: (Pair a ~> f) -> (a -> Shape f)
+adjunctPairShape h a = Shape (h (a,()))
+
+adjunctPairShape' :: Functor f => (a -> Shape f) -> (Pair a ~> f)
+adjunctPairShape' g (a,b) = b <$ getShape (g a)
+
+adjunctShapeConst :: Functor f => (Shape f -> a) -> (f ~> Const a)
+adjunctShapeConst h fb = Const $ h (Shape (() <$ fb))
+
+adjunctShapeConst' :: (f ~> Const a) -> (Shape f -> a)
+adjunctShapeConst' g (Shape f1) = getConst $ g f1
+
+adjunctConstEmptied :: (Const a ~> f) -> a -> Emptied f
+adjunctConstEmptied h a = Emptied (h (Const a))
+
+adjunctConstEmptied' :: Functor f => (a -> Emptied f) -> (Const a ~> f)
+adjunctConstEmptied' g (Const a) = vacuous $ getEmptied (g a)
+
+
+-- | @adjunctΓY :: (Γ f `'Control.Category.Op'` a) -> (f ~> Y a)@
+adjunctΓY :: (a -> Γ f) -> (f ~> Y a)
+adjunctΓY h fb a = getΓ (h a) fb
+
+-- | @adjunctΓY' :: (f ~> Y a) -> (Γ f `Control.Category.Op` a)@ 
+adjunctΓY' :: (f ~> Y a) -> (a -> Γ f)
+adjunctΓY' g a = Γ (\fb -> g fb a)
+
+-- * Monads and Comonads from these adjunctions
+
+-- | @J0 mm ~ Emptied ∘ mm ∘ Const@
+newtype J0 mm a = J0 { runJ0 :: mm (Const a) Void }
+
+instance FFunctor mm => Functor (J0 mm) where
+  fmap f = J0 . ffmap (first f) . runJ0
+
+instance FMonad mm => Applicative (J0 mm) where
+  pure = J0 . fpure . Const
+  (<*>) = ap
+
+instance FMonad mm => Monad (J0 mm) where
+  ma >>= k = J0 $ fbind (adjunctConstEmptied' (coerce . k)) (runJ0 ma)
+
+-- | @K ww ~ Shape ∘ ww ∘ Const@ 
+newtype K1 ww a = K1 { runK1 :: ww (Const a) () }
+
+instance FFunctor ww => Functor (K1 ww) where
+  fmap f = K1 . ffmap (first f) . runK1
+
+instance FComonad ww => Comonad (K1 ww) where
+  extract :: K1 ww a -> a
+  extract = getConst . fextract . runK1
+
+  extend :: (K1 ww a -> b) -> K1 ww a -> K1 ww b
+  extend h = K1 . fextend (adjunctShapeConst (h . coerce)). runK1
+
+-- | @J1 mm ~ Emptied ∘ mm ∘ Const@
+--
+-- Also, @J1 ~ 'Control.Monad.Trail.Trail'@
+newtype J1 mm a = J1 { runJ1 :: mm (Pair a) () }
+
+instance FFunctor mm => Functor (J1 mm) where
+  fmap f = J1 . ffmap (first f) . runJ1
+
+instance FMonad mm => Applicative (J1 mm) where
+  pure = J1 . fpure . (, ())
+  (<*>) = ap
+
+instance FMonad mm => Monad (J1 mm) where
+  ma >>= k = J1 $ fbind (adjunctPairShape' (coerce . k)) (runJ1 ma)
+
+-- | @RR ww ~ Γ ∘ ww ∘ Y@
+newtype RR ww a = RR { runRR :: Γ (ww (Y a)) }
+
+instance FFunctor ww => Functor (RR ww) where
+  fmap f = RR . mapΓ (ffmap (mapY f)) . runRR
+
+instance FComonad ww => Applicative (RR ww) where
+  pure a = RR $ Γ $ \wwk -> fextract wwk a
+  (<*>) = ap
+
+instance FComonad ww => Monad (RR ww) where
+  ma >>= k = RR $ Γ $ \wwk -> getΓ (runRR ma) (fextend (adjunctΓY (runRR . k)) wwk)
+
+-- | @RR ww@ specialized to @ww = Precompose w@
+newtype R w a = R { runR :: forall r. (a -> w r) -> r }
+
+instance Functor (R w) where
+  fmap f rw = R $ \cont -> runR rw (cont . f)
+
+instance Comonad w => Applicative (R w) where
+  pure a = R $ \cont -> extract (cont a)
+  (<*>) = ap
+
+instance Comonad w => Monad (R w) where
+  rw >>= k = R $ \cont -> runR rw (\a -> runR (k a) (duplicate . cont))
diff --git a/functor-monad.cabal b/functor-monad.cabal
--- a/functor-monad.cabal
+++ b/functor-monad.cabal
@@ -7,7 +7,7 @@
 
   @FMonad@ is a type class for monads in the category of @Functor@s.
 
-version:             0.1.1.0
+version:             0.1.1.1
 license:             BSD-3-Clause
 license-file:        LICENSE
 author:              Koji Miyazato
@@ -26,6 +26,7 @@
     FFunctor,
     FFunctor.FCompose,
     FFunctor.Adjunction,
+
     FMonad,
     FMonad.FFree,
     FMonad.FreeT,
@@ -72,6 +73,7 @@
   type:               exitcode-stdio-1.0
   hs-source-dirs:     examples
   main-is:            ListTVia.hs
-  build-depends:      base, transformers, free, functor-monad
+  other-modules:      TrailAsAdjunction
+  build-depends:      base, transformers, free, kan-extensions, comonad, functor-monad
   ghc-options:        -Wall -Wwarn=unused-packages
   default-language:   Haskell2010
diff --git a/src/Control/Monad/Trail.hs b/src/Control/Monad/Trail.hs
--- a/src/Control/Monad/Trail.hs
+++ b/src/Control/Monad/Trail.hs
@@ -16,13 +16,13 @@
 --
 -- @Trail mm@ can become variantions of @Monad@ for different @FMonad mm@.
 --
--- * @mm = 'FMonad.Compose.ComposePost' m@
+-- * @mm = 'Data.Functor.Compose.Compose' m@
 --
---     For any @Monad m@, @Trail (ComposePost m)@ is isomorphic to @m@.
+--     For any @Monad m@, @Trail (Compose m)@ is isomorphic to @m@.
 --
 --     @
---     Trail (ComposePost m) a
---       ~ ComposePost m ((,) a) ()
+--     Trail (Compose m) a
+--       ~ Compose m ((,) a) ()
 --       ~ m (a, ())
 --       ~ m a
 --     @
diff --git a/src/FStrong.hs b/src/FStrong.hs
--- a/src/FStrong.hs
+++ b/src/FStrong.hs
@@ -70,7 +70,7 @@
   -- >            v                           fstrength                               |
   -- >  ff g ⊗ (h ⊗ k) --------------------------------------------------->  ff (g ⊗ (h ⊗ k))
   --
-  -- For readability, an infix operator @(⊗) was used instead of the type constructor @Day@.
+  -- For readability, an infix operator @(⊗)@ was used instead of the type constructor @Day@.
   fstrength :: (Functor g) => Day (ff g) h ~> ff (Day g h)
   fstrength (Day ffg h op) =
     runCurried (mapCurried (unapplied h)) (fmap op ffg)