===== Finite sum over a monoid =====
==== Function ====
| @#55CCEE: context     | @#55CCEE: $ \langle\!\langle M,* \rangle\!\rangle$ ... monoid |
| @#BBDDEE: let         | @#BBDDEE: $e$ ... unit of $\langle\!\langle M,* \rangle\!\rangle$ |
| @#FF9944: definition  | @#FF9944: $\sum^n:\prod_{S:\mathrm{Sequence}(M)}\mathrm{range}(\mathrm{length}(S))\to M$ |
| @#FF9944: definition  | @#FF9944: $\sum_{k=1}^n\ S_k:= \begin{cases} e & \mathrm{if}\ n=0\\\\ \left(\sum_{k=1}^{n-1}\ S_k\right)\ *\ S_n & \mathrm{else} \end{cases}$ |

-----
=== Discussion ===
Here $\prod_{S:\mathrm{Sequence}(M)}$ is a dependent function type former.

-----
=== Context ===
[[Monoid]],
[[Sequence length]]
=== Requirements ===
[[Sequence length]]