Fix 315--325.

1 files changed, 4 insertions, 9 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index e4465fd..689a9bf 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -132,15 +132,10 @@ are standard, as are the rules for variables and let bindings. The two
 new operators, \roll{} and \foldkw{}, introduce values of an inductive
 type \(\mu X. A\). The \roll{} operator takes a vessel of shape \(A\)
 filled with inductive components and rolls it into an inductive
-value. The \foldkw{} operator takes a target inductive value and a
-body, which tranforms the induction hypothesis into a value of the
-motive type. By recursively applying the body to the inductive
-components of the target, the \foldkw{} computes a result.
-
-For those who are categorically minded, \roll{} is an algebraic map
-for a weak initial \(A\)-algebra (viewing \(A\) as an endofunctor) and
-\foldkw{} is the weak universal map. The structure is weak-universal
-as it is not guaranteed to be unique, only to exist.
+value. The \foldkw{} operator takes a target value and a body which
+transforms an induction hypothesis into a value of the motive type. By
+recursively applying the body to the inductive components of the
+target, the \foldkw{} computes a result.
 
 As a concrete example, consider the type \(\mathsf{Tree} \coloneq \mu X. 1 + (X \times
 X)\) of unlabeled binary trees. By combining injections with \roll{}, we can