    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Vectors defined as functions from a finite set to a type.
    ------------------------------------------------------------------------

    -- This implementation is designed for reasoning about fixed-size
    -- vectors where ease of retrieval of elements is prioritised.

    -- See `Data.Vec` for an alternative implementation using inductive
    -- data-types, which is more suitable for reasoning about vectors that
    -- will grow or shrink in size.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Vec.Functional where

    open import Data.Fin.Base
    open import Data.List.Base as L using (List)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
    open import Data.Product.Base using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
    open import Data.Vec.Base as V using (Vec)
    open import Function.Base using (_∘_; const; flip; _ˢ_; id)
    open import Level using (Level)

    infixr 5 _∷_ _++_
    infixl 4 _⊛_
    infixl 1 _>>=_

    private
      variable
        a b c : Level
        A B C : Set a
        m n : ℕ

    ------------------------------------------------------------------------
    -- Definition

    Vector : Set a → ℕ → Set a
    Vector A n = Fin n → A

    ------------------------------------------------------------------------
    -- Conversion

    toVec : Vector A n → Vec A n
    toVec = V.tabulate

    fromVec : Vec A n → Vector A n
    fromVec = V.lookup

    toList : Vector A n → List A
    toList = L.tabulate

    fromList : ∀ (xs : List A) → Vector A (L.length xs)
    fromList = L.lookup

    ------------------------------------------------------------------------
    -- Basic operations

    [] : Vector A zero
    [] ()

    _∷_ : A → Vector A n → Vector A (suc n)
    (x ∷ xs) zero    = x
    (x ∷ xs) (suc i) = xs i

    length : Vector A n → ℕ
    length {n = n} _ = n

    head : Vector A (suc n) → A
    head xs = xs zero

    tail : Vector A (suc n) → Vector A n
    tail xs = xs ∘ suc

    uncons : Vector A (suc n) → A × Vector A n
    uncons xs = head xs , tail xs

    replicate : (n : ℕ) → A → Vector A n
    replicate n = const

    insertAt : Vector A n → Fin (suc n) → A → Vector A (suc n)
    insertAt {n = n}     xs zero    v zero    = v
    insertAt {n = n}     xs zero    v (suc j) = xs j
    insertAt {n = suc n} xs (suc i) v zero    = head xs
    insertAt {n = suc n} xs (suc i) v (suc j) = insertAt (tail xs) i v j

    removeAt : Vector A (suc n) → Fin (suc n) → Vector A n
    removeAt t i = t ∘ punchIn i

    updateAt : Vector A n → Fin n → (A → A) → Vector A n
    updateAt {n = suc n} xs zero    f zero    = f (head xs)
    updateAt {n = suc n} xs zero    f (suc j) = xs (suc j)
    updateAt {n = suc n} xs (suc i) f zero    = head xs
    updateAt {n = suc n} xs (suc i) f (suc j) = updateAt (tail xs) i f j

    ------------------------------------------------------------------------
    -- Transformations

    map : (A → B) → ∀ {n} → Vector A n → Vector B n
    map f xs = f ∘ xs

    _++_ : Vector A m → Vector A n → Vector A (m ℕ.+ n)
    _++_ {m = m} xs ys i = [ xs , ys ] (splitAt m i)

    concat : Vector (Vector A m) n → Vector A (n ℕ.* m)
    concat {m = m} xss i = uncurry (flip xss) (quotRem m i)

    foldr : (A → B → B) → B → ∀ {n} → Vector A n → B
    foldr f z {n = zero}  xs = z
    foldr f z {n = suc n} xs = f (head xs) (foldr f z (tail xs))

    foldl : (B → A → B) → B → ∀ {n} → Vector A n → B
    foldl f z {n = zero}  xs = z
    foldl f z {n = suc n} xs = foldl f (f z (head xs)) (tail xs)

    rearrange : (Fin m → Fin n) → Vector A n → Vector A m
    rearrange r xs = xs ∘ r

    _⊛_ : Vector (A → B) n → Vector A n → Vector B n
    _⊛_ = _ˢ_

    _>>=_ : Vector A m → (A → Vector B n) → Vector B (m ℕ.* n)
    xs >>= f = concat (map f xs)

    zipWith : (A → B → C) → ∀ {n} → Vector A n → Vector B n → Vector C n
    zipWith f xs ys i = f (xs i) (ys i)

    unzipWith : (A → B × C) → Vector A n → Vector B n × Vector C n
    unzipWith f xs = proj₁ ∘ f ∘ xs , proj₂ ∘ f ∘ xs

    zip : Vector A n → Vector B n → Vector (A × B) n
    zip = zipWith _,_

    unzip : Vector (A × B) n → Vector A n × Vector B n
    unzip = unzipWith id

    take : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A m
    take _ {n = n} xs = xs ∘ (_↑ˡ n)

    drop : ∀ m {n} → Vector A (m ℕ.+ n) → Vector A n
    drop m xs = xs ∘ (m ↑ʳ_)

    reverse : Vector A n → Vector A n
    reverse xs = xs ∘ opposite

    init : Vector A (suc n) → Vector A n
    init xs = xs ∘ inject₁

    last : Vector A (suc n) → A
    last {n = n} xs = xs (fromℕ n)

    transpose : Vector (Vector A n) m → Vector (Vector A m) n
    transpose = flip

    ------------------------------------------------------------------------
    -- DEPRECATED
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.0

    remove : Fin (suc n) → Vector A (suc n) → Vector A n
    remove = flip removeAt
    {-# WARNING_ON_USAGE remove
    "Warning: remove was deprecated in v2.0.
    Please use removeAt instead.
    NOTE: argument order has been flipped."
    #-}
    insert = insertAt
    {-# WARNING_ON_USAGE insert
    "Warning: insert was deprecated in v2.0.
    Please use insertAt instead."
    #-}