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