Justify why only `length` and `index`.

1 files changed, 13 insertions, 5 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 43acd65..5dbe00f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -308,11 +308,19 @@ non-empty list. We retreive the head by calling the index function
 with index zero. The tail is one shorter that the initial list, and
 the index function is shifted by one too.
 
-\TODO{
-  \begin{itemize}
-    \item explain why a list is a pair of length and index function
-  \end{itemize}
-}
+We have shown that \(\mathsf{length}\) and \(\mathsf{index}\) are
+sufficient to produce an eliminator encoding for lists. We cannot add
+\(\mathsf{nil}\), \(\mathsf{cons}\) nor \(\mathsf{snoc}\) to the set
+of eliminators, as these all construct lists. Similarly pattern
+matching ``constructs'' the tail of a non-empty list. The only other
+operator we could possibly add as an eliminator is
+\(\mathsf{max}\). There are two main reasons we have not done
+this. Firstly, \(\mathsf{max}\) is only defined on lists of naturals,
+so we would end up with a non-uniform representation of
+lists. Secondly, the maximum is only computed for a small number of
+lists. In our running examples we compute the maximum only twice,
+whereas we use lists thoughout. Carrying redundant data around for an
+infrequent operation is inefficient and would complicate the encoding.
 
 After phase three, our example for \systemtinline{balanced} beta
 reduces to the following: