From c96076007468bc5636ceaa2c5de97238a69f639e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 18:42:48 +0100
Subject: Give (weak) justification for adding `snoc`.

---
 sec/encoding.ltx | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'sec/encoding.ltx')

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}
 }
-- 
cgit v1.2.3

