finite_sum_over_a

Finite sum over a monoid

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}$

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