    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties related to Pointwise
    ------------------------------------------------------------------------

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

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

    open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
    open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ)
    open import Data.Nat.Base using (ℕ; zero; suc)
    open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
    open import Data.Product.Relation.Binary.Pointwise.NonDependent
      using () renaming (Pointwise to ×-Pointwise)
    open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
    open import Data.Vec.Functional as VF hiding (map)
    open import Data.Vec.Functional.Relation.Binary.Pointwise
    open import Function.Base using (const; _∘_)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel; REL)
    open import Relation.Binary.Bundles using (Setoid; DecSetoid)
    open import Relation.Binary.Structures
      using (IsEquivalence; IsDecEquivalence)
    open import Relation.Binary.Definitions
      using (Reflexive; Transitive; Symmetric; Decidable)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)

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

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

    module _ {R : Rel A ℓ} where

      refl : Reflexive R → ∀ {n} → Reflexive (Pointwise R {n})
      refl r i = r

      sym : Symmetric R → ∀ {n} → Symmetric (Pointwise R {n})
      sym s xsys i = s (xsys i)

      trans : Transitive R → ∀ {n} → Transitive (Pointwise R {n})
      trans t xsys yszs i = t (xsys i) (yszs i)

      decidable : Decidable R → ∀ {n} → Decidable (Pointwise R {n})
      decidable r? xs ys = all? λ i → r? (xs i) (ys i)

    ------------------------------------------------------------------------
    -- Structures

      isEquivalence : IsEquivalence R → ∀ n → IsEquivalence (Pointwise R {n})
      isEquivalence isEq n = record
        { refl  = refl  Eq.refl
        ; sym   = sym   Eq.sym
        ; trans = trans Eq.trans
        } where module Eq = IsEquivalence isEq

      isDecEquivalence : IsDecEquivalence R →
                         ∀ n → IsDecEquivalence (Pointwise R {n})
      isDecEquivalence isDecEq n = record
        { isEquivalence = isEquivalence Eq.isEquivalence n
        ; _≟_           = decidable Eq._≟_
        } where module Eq = IsDecEquivalence isDecEq

    ------------------------------------------------------------------------
    -- Bundles

    setoid : Setoid a ℓ → ℕ → Setoid a ℓ
    setoid S n = record
      { isEquivalence = isEquivalence S.isEquivalence n
      } where module S = Setoid S

    decSetoid : DecSetoid a ℓ → ℕ → DecSetoid a ℓ
    decSetoid S n = record
      { isDecEquivalence = isDecEquivalence S.isDecEquivalence n
      } where module S = DecSetoid S

    ------------------------------------------------------------------------
    -- map

    module _ {R : REL A B r} {S : REL A′ B′ s} {f : A → A′} {g : B → B′} where

      map⁺ : (∀ {x y} → R x y → S (f x) (g y)) →
             ∀ {n} {xs : Vector A n} {ys : Vector B n} →
             Pointwise R xs ys → Pointwise S (VF.map f xs) (VF.map g ys)
      map⁺ f rs i = f (rs i)

    ------------------------------------------------------------------------
    -- head

    module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where

      head⁺ : Pointwise R xs ys → R (head xs) (head ys)
      head⁺ rs = rs zero

    ------------------------------------------------------------------------
    -- tail

    module _ (R : REL A B r) {n} {xs : Vector A (suc n)} {ys} where

      tail⁺ : Pointwise R xs ys → Pointwise R (tail xs) (tail ys)
      tail⁺ rs = rs ∘ suc

    ------------------------------------------------------------------------
    -- _++_

    module _ (R : REL A B r) where

      ++⁺ : ∀ {m n xs ys xs′ ys′} →
            Pointwise R {n = m} xs ys → Pointwise R {n = n} xs′ ys′ →
            Pointwise R (xs ++ xs′) (ys ++ ys′)
      ++⁺ {m} rs rs′ i with splitAt m i
      ... | inj₁ i′ = rs i′
      ... | inj₂ j′ = rs′ j′

      ++⁻ˡ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
             Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs ys
      ++⁻ˡ {m} {n} _ _ rs i with rs (i ↑ˡ n)
      ... | r rewrite splitAt-↑ˡ m i n = r

      ++⁻ʳ : ∀ {m n} (xs : Vector A m) (ys : Vector B m) {xs′ ys′} →
             Pointwise R (xs ++ xs′) (ys ++ ys′) → Pointwise R xs′ ys′
      ++⁻ʳ {m} {n} _ _ rs i with rs (m ↑ʳ i)
      ... | r rewrite splitAt-↑ʳ m n i = r

      ++⁻ : ∀ {m n} xs ys {xs′ ys′} →
            Pointwise R (xs ++ xs′) (ys ++ ys′) →
            Pointwise R {n = m} xs ys × Pointwise R {n = n} xs′ ys′
      ++⁻ _ _ rs = ++⁻ˡ _ _ rs , ++⁻ʳ _ _ rs

    ------------------------------------------------------------------------
    -- replicate

    module _ {R : REL A B r} {x y n} where

      replicate⁺ : R x y → Pointwise R {n = n} (replicate n x) (replicate n y)
      replicate⁺ = const

    ------------------------------------------------------------------------
    -- _⊛_

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

      ⊛⁺ : ∀ {fs : Vector (A → A′) n} {gs : Vector (B → B′) n} →
           Pointwise (λ f g → ∀ {x y} → R x y → S (f x) (g y)) fs gs →
           ∀ {xs ys} → Pointwise R xs ys → Pointwise S (fs ⊛ xs) (gs ⊛ ys)
      ⊛⁺ rss rs i = (rss i) (rs i)

    ------------------------------------------------------------------------
    -- zipWith

    module _ {R : REL A B r} {S : REL A′ B′ s} {T : REL A″ B″ t} where

      zipWith⁺ : ∀ {n xs ys xs′ ys′ f f′} →
                 (∀ {x y x′ y′} → R x y → S x′ y′ → T (f x x′) (f′ y y′)) →
                 Pointwise R xs ys → Pointwise S xs′ ys′ →
                 Pointwise T (zipWith f xs xs′) (zipWith f′ {n = n} ys ys′)
      zipWith⁺ t rs ss i = t (rs i) (ss i)

    ------------------------------------------------------------------------
    -- zip

    module _ {R : REL A B r} {S : REL A′ B′ s} {n xs ys xs′ ys′} where

      zip⁺ : Pointwise R xs ys → Pointwise S xs′ ys′ →
             Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′)
      zip⁺ rs ss i = rs i , ss i

      zip⁻ : Pointwise (×-Pointwise R S) (zip xs xs′) (zip {n = n} ys ys′) →
             Pointwise R xs ys × Pointwise S xs′ ys′
      zip⁻ rss = proj₁ ∘ rss , proj₂ ∘ rss

    ------------------------------------------------------------------------
    -- foldr

    module _ {R : REL A B r} {S : REL A′ B′ s}
             {f : A → A′ → A′} {g : B → B′ → B′}
             where

      foldr-cong : (∀ {w x y z} → R w x → S y z → S (f w y) (g x z)) →
                   ∀ {d : A′} {e : B′} → S d e →
                   ∀ {n} {xs : Vector A n} {ys : Vector B n} →
                   Pointwise R xs ys → S (foldr f d xs) (foldr g e ys)
      foldr-cong fg-cong d~e {zero}  rss = d~e
      foldr-cong fg-cong d~e {suc n} rss =
        fg-cong (rss zero) (foldr-cong fg-cong d~e (rss ∘ suc))