## Finite sum over a monoid

### Function

 context $\langle\!\langle M,* \rangle\!\rangle$ … monoid let $e$ … unit of $\langle\!\langle M,* \rangle\!\rangle$ definition $\sum^n:\prod_{S:\mathrm{Sequence}(M)}\mathrm{range}(\mathrm{length}(S))\to M$ definition $\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.