Give the encoding of nil.

1 files changed, 10 insertions, 0 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 482c7b0..5537a2e 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -245,6 +245,16 @@ following operators for lists: \(\mathsf{nil}\), \(\mathsf{cons}\),
 operators using only the \(\mathsf{length}\) and \(\mathsf{index}\)
 eliminators.
 
+More formally, we encode the type \(\mathsf{List}~A\) by the type
+\(\nat \times (\nat \to A)\), where the first component is the length of the
+list and the second is the index function. We will justify using these
+eliminators by giving an encoding for each operator. Starting with the
+constructors, we can encode \(\mathsf{nil}\) by the pair \(\tuple{0,
+  \arb}\). The empty list has length zero, and as there are no valid
+indices, we can give an arbitrary indexing function. Recall that all
+System~T types are inhabited which allows us to construct this
+arbitrary value.
+
 \TODO{
   \begin{itemize}
     \item explain why a list is a pair of length and index function