From b1929bac3af5c9c8fc8a83e0d75edf98082cb7d2 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 16:49:11 +0100
Subject: Fix 315--325.

---
 sec/lang.ltx | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'sec/lang.ltx')

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

