Fix 831--899.

1 files changed, 14 insertions, 20 deletions

diff --git a/sec/reducer.ltx b/sec/reducer.ltx
index 2079e49..2a0b193 100644
--- a/sec/reducer.ltx
+++ b/sec/reducer.ltx
@@ -139,17 +139,13 @@ finite sums and products are over unlabelled lists of types instead of
 finite sets.
 
 Folds in \lang{} are destructive---the inductive components used to
-generate the induction hypothesis are unnamed. This has some
+generate the induction hypothesis are inaccessible. This has some
 interesting interactions with encoding the \(\mathsf{distrib}\) term
 in phase one, and implementing the \mapkw{} pseudo-operator in phase
-two. Both of these functions are defined by induction on types with
-motives that are functions returning terms. This means that the
-inductive hypothesis for each branch consists of a type constructor
-filled with some number functions. To construct a term, we need not
-only the subterms provided by the induction hypothesis, but we also
-need the types of those subterms. To preserve this typing information,
-both \(\mathsf{distrib}\) and \mapkw{} must return a pair of type and
-term.
+two. Both of these functions of the form \(\text{Type} \to \text{Env} \to
+\text{Term}\). Our term representations require type annotations but
+any subtypes are inaccessible. So, we program \(\mathsf{distrib}\) and
+\(\mathsf{map}\) to return a pair of term and type.
 
 \begin{listing}
   \begin{verbatim}
@@ -166,23 +162,21 @@ term.
 \end{listing}
 
 As a concrete example, consider the branch of \(\mathsf{distrib}\)
-over a function type, shown in \cref{lst:distrib-arrow}. The induction
-hypothesis is a pair of motives generated from the domain and
-codomain. The motive is a pair of functions. The \verb|Ty| component
-takes an environment and returns a compiled type. The \verb|Term|
-component takes an environment, a chosen type variable \verb|k| and a
-type \verb|S| and returns a term distributing an accumulator for
-\verb|S| at index \verb|k| outside of the type constructor. Ideally,
+over a function type, shown in \cref{lst:distrib-arrow}. The motive
+type is
+\verb|<Ty : List Type -> Type; Term: List Type -> Nat -> Type>|. The
+\verb|Ty| component is the result of type substitution and the
+\verb|Term| component is the result of \(\mathsf{distrib}\).  Ideally,
 we would only need the \verb|Term| component of the pair. However, the
-type annotations needed for the tuple force us to also compute the types.
+type annotations needed for the tuple force us to also compute the
+types.
 
 From a language design standpoint, we could have chosen that \foldkw{}
 is non-destructive. The inductive hypothesis would have the form
 \(\sub{A}{X/(\mu X. A) \times B}\) for shape \(A\) and motive \(B\). This is
 exactly as expressive as the chosen type, with inductive hypothesis
-\(\sub{A}{X/B}\). We chose to use the simpler motive inductive
-hypothesis for two reasons: it has a simpler categorical semantics;
-many folds do not need the non-destructive argument.
+\(\sub{A}{X/B}\). We chose to use the simpler motive as many folds do
+not need the non-destructive argument.
 
 \subsection{Composing the Two Programs}