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

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

    module Data.Vec.Functional.Relation.Binary.Pointwise where

    open import Data.Vec.Functional as VF hiding (map)
    open import Level using (Level)
    open import Relation.Binary.Core using (REL; _⇒_)

    private
      variable
        a b r s ℓ : Level
        A : Set a
        B : Set b

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

    Pointwise : REL A B ℓ → ∀ {n} → Vector A n → Vector B n → Set ℓ
    Pointwise R xs ys = ∀ i → R (xs i) (ys i)

    ------------------------------------------------------------------------
    -- Operations

    module _ {R : REL A B r} {S : REL A B s} where

      map : R ⇒ S → ∀ {n} → Pointwise R ⇒ Pointwise S {n = n}
      map f rs i = f (rs i)