- indexNaturality : (i : Fin n) -> (f : (a -> b)) -> (xs : Vect n a) -> index i (map f xs) = f (index i xs)
`index i : Vect n a -> a` is a natural transformation
- indexRange : (i : Fin n) -> index i range = i
`range` tabulates the identity function (by definition)
- indexReplicate : (i : Fin n) -> (x : a) -> index i (replicate n x) = x
Replication tabulates the constant function
The `i`-th vector in a transposed matrix is the vector of `i`-th components
- recallElem : Elem x xs -> a
Recall an element by its position, as we may not have the element
at runtime
- recallElemSpec : (pos : Elem x xs) -> recallElem pos = x
Recalling by a position of `x` does yield `x`