    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Pointwise lifting of relations over Vector
    ------------------------------------------------------------------------

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

    open import Data.Nat.Base using (ℕ)
    open import Data.Vec.Functional hiding (map)
    open import Data.Vec.Functional.Relation.Binary.Pointwise
      using (Pointwise)
    import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as PW
    open import Level using (Level)
    open import Relation.Binary.Core using (_⇒_)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)
    open import Relation.Binary.Definitions
      using (Reflexive; Symmetric; Transitive)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)

    module Data.Vec.Functional.Relation.Binary.Equality.Setoid
      {a ℓ} (S : Setoid a ℓ) where

    open Setoid S renaming (Carrier to A)

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

    infix 4 _≋_

    _≋_ : ∀ {n} → Vector A n → Vector A n → Set ℓ
    _≋_ = Pointwise _≈_

    ------------------------------------------------------------------------
    -- Relational properties
    ------------------------------------------------------------------------

    ≋-refl : ∀ {n} → Reflexive (_≋_ {n = n})
    ≋-refl {n} = PW.refl {R = _≈_} refl

    ≋-reflexive : ∀ {n} → _≡_ ⇒ (_≋_ {n = n})
    ≋-reflexive ≡.refl = ≋-refl

    ≋-sym : ∀ {n} → Symmetric (_≋_ {n = n})
    ≋-sym = PW.sym {R = _≈_} sym

    ≋-trans : ∀ {n} → Transitive (_≋_ {n = n})
    ≋-trans = PW.trans {R = _≈_} trans

    ≋-isEquivalence : ∀ n → IsEquivalence (_≋_ {n = n})
    ≋-isEquivalence = PW.isEquivalence isEquivalence

    ≋-setoid : ℕ → Setoid _ _
    ≋-setoid = PW.setoid S

    ------------------------------------------------------------------------
    -- Properties
    ------------------------------------------------------------------------

    open PW public
      using
      ( map⁺
      ; head⁺; tail⁺
      ; ++⁺; ++⁻ˡ; ++⁻ʳ; ++⁻
      ; replicate⁺
      ; ⊛⁺
      ; zipWith⁺; zip⁺; zip⁻
      )

    foldr-cong : ∀ {f g} → (∀ {w x y z} → w ≈ x → y ≈ z → f w y ≈ g x z) →
                 ∀ {d e : A} → d ≈ e →
                 ∀ {n} {xs ys : Vector A n} → xs ≋ ys →
                 foldr f d xs ≈ foldr g e ys
    foldr-cong = PW.foldr-cong