module Data.Vec.Properties where

# Properties of vectorsπ

tabulate-lookup : (xs : Vec A n) β tabulate (lookup xs) β‘ xs tabulate-lookup [] = refl tabulate-lookup (x β· xs) = ap (x β·_) (tabulate-lookup xs) lookup-tabulate : (xs : Fin n β A) (i : Fin n) β lookup (tabulate xs) i β‘ xs i lookup-tabulate xs fzero = refl lookup-tabulate xs (fsuc i) = lookup-tabulate (Ξ» x β xs (fsuc x)) i lookup-is-equiv : is-equiv (lookup {A = A} {n}) lookup-is-equiv = is-isoβis-equiv $ iso tabulate (Ξ» x β funext (lookup-tabulate x)) tabulate-lookup module Lookup {β} {A : Type β} {n : Nat} = Equiv (lookup {A = A} {n} , lookup-is-equiv) map-lookup : β (f : A β B) (xs : Vec A n) i β lookup (Vec.map f xs) i β‘ f (lookup xs i) map-lookup f (x β· xs) fzero = refl map-lookup f (x β· xs) (fsuc i) = map-lookup f xs i map-id : (xs : Vec A n) β Vec.map (Ξ» x β x) xs β‘ xs map-id xs = Lookup.injectiveβ (funext Ξ» i β map-lookup _ xs i) refl map-comp : (xs : Vec A n) (f : A β B) (g : B β C) β Vec.map (Ξ» x β g (f x)) xs β‘ Vec.map g (Vec.map f xs) map-comp xs f g = Lookup.injective $ funext Ξ» i β lookup (Vec.map (Ξ» x β g (f x)) xs) i β‘β¨ map-lookup (Ξ» x β g (f x)) xs i β©β‘ g (f (lookup xs i)) β‘Λβ¨ ap g (map-lookup f xs i) β©β‘Λ g (lookup (Vec.map f xs) i) β‘Λβ¨ map-lookup g (Vec.map f xs) i β©β‘Λ lookup (Vec.map g (Vec.map f xs)) i β