diff options
author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-25 17:18:35 +0100 |
---|---|---|
committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-25 17:18:35 +0100 |
commit | ad1fc4da5ba668c2fdf0150e59ff5bd2e3ec191e (patch) | |
tree | 7baccd3ed12b483f2f1c1bf64968ff17cd1e9b3d /sec | |
parent | d0f32b0ba0369b14291862f82659c46e864a4791 (diff) |
Fix map syntax.
Diffstat (limited to 'sec')
-rw-r--r-- | sec/lang.ltx | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/sec/lang.ltx b/sec/lang.ltx index 02575d8..b26359f 100644 --- a/sec/lang.ltx +++ b/sec/lang.ltx @@ -161,9 +161,9 @@ our chosen variable \(X \in \Psi\). \maptm{X}{X} &\coloneq \lambda f, x. f~x \\ \maptm{X}{Y} &\coloneq \lambda f, x. x \qquad (X \neq Y)\\ \maptm{X}{A \to B} &\coloneq \lambda f, x. x \\ - \maptm{X}{\prod_i A_i} &\coloneq \lambda f, x. \tuple{\rangeover{\maptm{X}{A_i}~f~x.i}{i}} \\ - \maptm{X}{\sum_i A_i} &\coloneq - \lambda f, x. \casetm{x}{\tuple{i,x_i}}{\tuple{i, \maptm{X}{A_i}~f~x_i}}{i} \\ + \maptm{X}{\prod_{\ell \in I} A_\ell} &\coloneq \lambda f, x. \tuple{\rangeover{\ell : \maptm{X}{A_\ell}~f~x.\ell}{\ell}} \\ + \maptm{X}{\sum_{\ell \in I} A_\ell} &\coloneq + \lambda f, x. \casetm{x}{\ell~x_\ell}{\ell~(\maptm{X}{A_i}~f~x_\ell)}{\ell} \\ \maptm{X}{\mu Y. A} &\coloneq \lambda f, x. \dofold{x}{y}{\roll~(\maptm{X}{\sub{A}{Y/\mu Y. \sub{A}{X/C}}}~f~y)} |