diff options
Diffstat (limited to 'sec/lang.ltx')
| -rw-r--r-- | sec/lang.ltx | 13 |
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 |