| 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.