it must determine the shape of the data-structure returned and the data in any position in the shape returned must come from a definite position in the given shape.

-   The head function, sending a non-empty list to a single data item, is determined by the maps $t : {\mathsf{Nat}}\to 1$ and $q : \Pi {\{s : {\mathsf{Nat}}\}}.\, 1 \to {\mathsf{Fin}}\, (s+1)$ defined by $t\, \_ =
    {{\ast}}$ and $q\, {{\ast}}= 0$.

-   The tail function, sending a non-empty list to a list, is represented by $t : {\mathsf{Nat}}\to {\mathsf{Nat}}$ and $q : \Pi {\{s :
      {\mathsf{Nat}}\}}.\, {\mathsf{Fin}}\, s \to {\mathsf{Fin}}\, (s+1)$ defined by $t\, s = s $ and $q\,
    p = p + 1$.

-   For the function dropping every second element of a non-empty list, the shape and position maps $t : {\mathsf{Nat}}\to {\mathsf{Nat}}$ and $q
    : \Pi {\{s : {\mathsf{Nat}}\}}.\, {\mathsf{Fin}}\, (s \div 2 + 1) \to {\mathsf{Fin}}\, (s + 1)$ are $t\, s = s \div 2$ and $q\, p = p * 2$.

-   For self-append of a non-empty list, they are $t : {\mathsf{Nat}}\to
      {\mathsf{Nat}}$ and $q : \Pi {\{s : {\mathsf{Nat}}\}}.\, {\mathsf{Fin}}\, (s * 2 + 2) \to {\mathsf{Fin}}\, (s +
      1)$ 