Give (weak) justification for adding `snoc`.

1 files changed, 7 insertions, 1 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 1063ba7..bf2c96e 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -175,10 +175,16 @@ X)\) of countable trees. To compute the recursive depth, we need to
 compute the maximum of a countable sequence, which is impossible in
 general. Thus we cannot encode such infinite types.
 
+Adding the \(\mathsf{snoc}\) operator may at first seem
+counterproductive; we want to encode away inductive types and
+recursion, yet \(\mathsf{snoc}\) is naively a recursion over an
+inductive type. Fortunately there exist encodings for lists such that
+not only does \(\mathsf{snoc}\) avoid recursion, but it is also as
+performant as cons.
+
 \TODO{
   \begin{itemize}
     \item justify the head operator
-    \item justify the snoc operator
     \item justify the arb operator
   \end{itemize}
 }