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