Idris2Doc : Data.Vect.Properties.Map

# Data.Vect.Properties.Map

```Properties of Data.Vect.map
```

## Definitions

`mapId : (xs : Vect n a) -> map id xs = xs`
`  `map` functoriality: identity preservation`

Visibility: export
`indexMapWithPos : (f : (Fin n -> a -> b)) -> (xs : Vect n a) -> (i : Fin n) -> index i (mapWithPos f xs) = f i (index i xs)`
`  `mapWtihPos f` represents post-composition the tabulated function `f``

Visibility: export
`mapTabulate : (f : (a -> b)) -> (g : (Fin n -> a)) -> tabulate (f . g) = map f (tabulate g)`
`  `tabulate : (Fin n ->) -> Vect n` is a natural transformation`

Visibility: export
`tabulateConstantly : (x : a) -> tabulate (const x) = replicate len x`
`  Tabulating with the constant function is replication`

Visibility: export
`mapRestrictedExtensional : (f : (a -> b)) -> (g : (a -> b)) -> (xs : Vect n a) -> ((i : Fin n) -> f (index i xs) = g (index i xs)) -> map f xs = map g xs`
`  It's enough that two functions agree on the elements of a vector for the maps to agree`

Visibility: export
`mapExtensional : (f : (a -> b)) -> (g : (a -> b)) -> ((x : a) -> f x = g x) -> (xs : Vect n a) -> map f xs = map g xs`
`  function extensionality is a congruence wrt map`

Visibility: export
`mapFusion : (f : (b -> c)) -> (g : (a -> b)) -> (xs : Vect n a) -> map f (map g xs) = map (f . g) xs`
`  map-fusion property for vectors up to function extensionality`

Visibility: export
`mapWithElemExtensional : (xs : Vect n a) -> (f : ((x : a) -> (0 _ : Elem x xs) -> b)) -> (g : ((x : a) -> (0 _ : Elem x xs) -> b)) -> ((x : a) -> (0 pos : Elem x xs) -> f x pos = g x pos) -> mapWithElem xs f = mapWithElem xs g`
`  function extensionality is a congruence wrt mapWithElem`

Visibility: export