diff --git a/sofp-src/sofp-transformers.lyx b/sofp-src/sofp-transformers.lyx
index 9667c8960..18aa01d08 100644
--- a/sofp-src/sofp-transformers.lyx
+++ b/sofp-src/sofp-transformers.lyx
@@ -13950,11 +13950,84 @@ noprefix "false"
 \end_inset
 
  summarizes various effectful operations for some well-known monads.
- The choice of operations appears to be random, not following any principle
+\begin_inset Foot
+status open
+
+\begin_layout Plain Layout
+The table was compiled using the 
+\family typewriter
+cats-mtl
+\family default
+ documentation and the papers 
+\begin_inset Quotes eld
+\end_inset
+
+
+\emph on
+Monad transformers and modular interpreters
+\emph default
+
+\begin_inset Quotes erd
+\end_inset
+
+ (see 
+\family typewriter
+
+\begin_inset CommandInset href
+LatexCommand href
+target "http://web.cecs.pdx.edu/~mpj/pubs/modinterp.html"
+literal "false"
+
+\end_inset
+
+
+\family default
+) and 
+\begin_inset Quotes eld
+\end_inset
+
+
+\emph on
+Modular monad transformers
+\emph default
+
+\begin_inset Quotes erd
+\end_inset
+
+ (see 
+\family typewriter
+
+\begin_inset CommandInset href
+LatexCommand href
+target "https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.5365"
+literal "false"
+
+\end_inset
+
+
+\family default
+).
+\end_layout
+
+\end_inset
+
+ The choice of operations appears to be heuristic, not following any principle
  or system.
  It is not obvious in advance what operations will be useful or necessary
  in practical tasks involving a given monad.
- (Do we need an extra filtering operation for the 
+ (Do we need a 
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+filter
+\end_layout
+
+\end_inset
+
+ operation for the 
 \begin_inset listings
 inline true
 status open
@@ -13966,18 +14039,17 @@ Either
 
 \end_inset
 
- monad?) So, different libraries choose different sets of supported operations.
+ monad?) Different libraries choose different sets of supported operations.
  However, adding a new operation to a monad in an MTL-style library requires
  rewriting the typeclasses involving that monad.
- Users of the library who cannot modify the library code will be unable
- to add new operations.
+ Users who cannot modify the library code will be unable to add new operations.
 \end_layout
 
 \begin_layout Standard
-The third problem is the difficulty in lifting certain operations to certain
- monad transformers.
- So far, the examples in this subsection were limited to effectful operations
- with type signatures of the form 
+The third problem is the lack of a general method of lifting effectful operation
+s to arbitrary monad transformers.
+ So far, the examples in this subsection were limited to operations with
+ type signatures of the form 
 \begin_inset Formula $L^{A}$
 \end_inset
 
@@ -13986,7 +14058,7 @@ The third problem is the difficulty in lifting certain operations to certain
 \end_inset
 
 .
- Operations of these types are lifted from the monad 
+ All operations of this form are lifted from the monad 
 \begin_inset Formula $L$
 \end_inset
 
@@ -13999,7 +14071,9 @@ The third problem is the difficulty in lifting certain operations to certain
 \end_inset
 
 .
- However, an operation called 
+ However, some operations have significantly different type signatures and
+ cannot be lifted to arbtirary monad stacks by composing with a lift function.
+ For instance, an operation called 
 \begin_inset listings
 inline true
 status open
@@ -14027,8 +14101,7 @@ Reader
 \begin_inset Formula $R\rightarrow\text{Reader}^{R,A}\rightarrow\text{Reader}^{R,A}$
 \end_inset
 
-.
- Because some 
+ where some some 
 \begin_inset listings
 inline true
 status open
@@ -14041,7 +14114,49 @@ Reader
 \end_inset
 
  monad values are used as arguments in that type signature (that is, in
- a contravariant position), it is impossible to lift the operation 
+ a contravariant position).
+ The withEnv operation cannot be lifted to a function of type 
+\begin_inset Formula $R\rightarrow P^{A}\rightarrow P^{A}$
+\end_inset
+
+ by using only a lift function 
+\begin_inset Formula $p:\text{Reader}^{R,A}\rightarrow P^{A}$
+\end_inset
+
+.
+ Similarly, the 
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+clear
+\end_layout
+
+\end_inset
+
+ operation for the 
+\begin_inset listings
+inline true
+status open
+
+\begin_layout Plain Layout
+
+Writer
+\end_layout
+
+\end_inset
+
+ monad has type signature 
+\begin_inset Formula $\text{Writer}^{W,A}\rightarrow\text{Writer}^{W,A}$
+\end_inset
+
+ and cannot be lifted to 
+\begin_inset Formula $P^{A}\rightarrow P^{A}$
+\end_inset
+
+ ***cle it is impossible to lift the operation 
 \begin_inset listings
 inline true
 status open
@@ -14057,11 +14172,7 @@ withEnv
 \begin_inset Formula $P^{A}$
 \end_inset
 
- by using only a lift function 
-\begin_inset Formula $p:\text{Reader}^{R,A}\rightarrow P^{A}$
-\end_inset
-
-.
+ .
  Lifting 
 \begin_inset listings
 inline true
@@ -14069,7 +14180,7 @@ status open
 
 \begin_layout Plain Layout
 
-withEnv
+clear
 \end_layout
 
 \end_inset
@@ -14097,14 +14208,18 @@ status open
 
 \begin_layout Plain Layout
 
-State
+Writer
 \end_layout
 
 \end_inset
 
-, needs code written specifically for that combination of monads.
- The required code length becomes quadratic in the number of supported monads.
- 
+***, needs code written specifically for that combination of monads.
+ The length of required custom code is quadratic in the number of supported
+ monads and linear in the number of operations.
+\end_layout
+
+\begin_layout Standard
+As an example, consider lifting withEnv to the stack 
 \end_layout
 
 \begin_layout Standard