Idris2Doc : Data.Vect.Properties.Map

# Data.Vect.Properties.Map

`Properties of Data.Vect.map`
indexMapWithPos : (f : (Finn -> a -> b)) -> (xs : Vectna) -> (i : Finn) -> indexi (mapWithPosfxs) = fi (indexixs)
`  `mapWtihPos f` represents post-composition the tabulated function `f``

mapExtensional : (f : (a -> b)) -> (g : (a -> b)) -> ((x : a) -> fx = gx) -> (xs : Vectna) -> mapfxs = mapgxs
`  function extensionality is a congruence wrt map`

mapFusion : (f : (b -> c)) -> (g : (a -> b)) -> (xs : Vectna) -> mapf (mapgxs) = map (f.g) xs
`  map-fusion property for vectors up to function extensionality`

mapId : (xs : Vectna) -> mapidxs = xs
`  `map` functoriality: identity preservation`

mapRestrictedExtensional : (f : (a -> b)) -> (g : (a -> b)) -> (xs : Vectna) -> ((i : Finn) -> f (indexixs) = g (indexixs)) -> mapfxs = mapgxs
`  It's enough that two functions agree on the elements of a vector for the maps to agree`

mapTabulate : (f : (a -> b)) -> (g : (Finn -> a)) -> tabulate (f.g) = mapf (tabulateg)
`  `tabulate : (Fin n ->) -> Vect n` is a natural transformation`

mapWithElemExtensional : (xs : Vectna) -> (f : ((x : a) -> (0 _ : Elemxxs) -> b)) -> (g : ((x : a) -> (0 _ : Elemxxs) -> b)) -> ((x : a) -> (0 pos : Elemxxs) -> fxpos = gxpos) -> mapWithElemxsf = mapWithElemxsg
`  function extensionality is a congruence wrt mapWithElem`

tabulateConstantly : (x : a) -> tabulate (constx) = replicatelenx
`  Tabulating with the constant function is replication`