1 files changed, 19 insertions, 14 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx
index da85b80..02575d8 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -152,20 +152,25 @@ can fold over a tree \(t\) with the term
 From the core of \lang{} we can further derive a number of useful
 operators. One of these is \mapkw, which lifts a function from type
 \(B \to C\) to \(\sub{A}{X/B} \to \sub{A}{X/C}\), acting on each component
-in the vessel. We define \(\maptm{X}{A}\) by induction on the
-well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), with our chosen
-variable \(X \in \Psi\).
-\begin{align*}
-  \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
-  \maptm{X}{Y} &\coloneq \lambda f, x. x && (X \neq Y)\\
-  \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
-  \maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\
-  \maptm{X}{\sum_i A_i} &\coloneq
-    \lambda f, x. \casetm{x}{\tuple{i,x_i}}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
-  \maptm{X}{\mu Y. A} &\coloneq
-  \lambda f, x.
-    \dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)}
-\end{align*}
+in a vessel. We define \(\maptm{X}{A}\) (shown in \cref{fig:map}) by
+induction on a well-formedness derivation \(\jdgmnt{ty}{\Psi}{A}\), with
+our chosen variable \(X \in \Psi\).
+
+\begin{figure}
+  \begin{align*}
+    \maptm{X}{X} &\coloneq \lambda f, x. f~x \\
+    \maptm{X}{Y} &\coloneq \lambda f, x. x \qquad (X \neq Y)\\
+    \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\
+    \maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\
+    \maptm{X}{\sum_i A_i} &\coloneq
+      \lambda f, x. \casetm{x}{\tuple{i,x_i}}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\
+    \maptm{X}{\mu Y. A} &\coloneq
+    \lambda f, x.
+      \dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)}
+  \end{align*}
+  \caption{Definition of the \mapkw{} meta-operator.}\label{fig:map}
+\end{figure}
+
 \begin{proposition}
 The following typing judgement for \mapkw{} is sound.
 \begin{prooftree*}