The Fin Type Family

Due by 10 February 2017

For a type $X$ and a natural number $n$, functions $Fin(n) \to X$ can be idnetified with vectors of length $n$ with values in $X$. We use this throughout.

1. Define a function that associates to each vector $v : Fin(n) \to X$, such that the length $n$ of $v$ is at least one, its first co-ordinate.
2. Define a function that concatenates vectors to give a vector of length $m + n$ given vectors of length $m$ and $n$.
3. Define a function that gives the sum of the co-ordinates of a function $x : Fin(n) \to \mathbb{N}$ for a natural number $n$, with the sum of the empty vector $0$. You may use addition of a pair of natural numbers (which is a function $\mathbb{N} \to \mathbb{N} \to \mathbb{N}$).