    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of unique vectors (setoid equality)
    ------------------------------------------------------------------------

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

    module Data.Vec.Relation.Unary.Unique.Setoid.Properties where

    open import Data.Fin.Base using (Fin; zero; suc)
    open import Data.Vec.Base as Vec
    open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
    import Data.Vec.Relation.Unary.All.Properties as All
    open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs)
    open import Data.Vec.Relation.Unary.Unique.Setoid
    import Data.Vec.Relation.Unary.AllPairs.Properties as AllPairs
    open import Data.Nat.Base using (ℕ; _+_)
    open import Function.Base using (_∘_; id)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
    open import Relation.Nullary.Negation using (contradiction; contraposition)

    private
      variable
        a b c p ℓ ℓ₁ ℓ₂ ℓ₃ : Level

    ------------------------------------------------------------------------
    -- Introduction (⁺) and elimination (⁻) rules for list operations
    ------------------------------------------------------------------------
    -- map

    module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where

      open Setoid S renaming (_≈_ to _≈₁_)
      open Setoid R renaming (_≈_ to _≈₂_)

      map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
             ∀ {n xs} → Unique S {n} xs → Unique R {n} (map f xs)
      map⁺ inj xs! = AllPairs.map⁺ (AllPairs.map (contraposition inj) xs!)

    ------------------------------------------------------------------------
    -- take & drop

    module _ (S : Setoid a ℓ) where

      drop⁺ : ∀ {n} m {xs} → Unique S {m + n} xs → Unique S {n} (drop m xs)
      drop⁺ = AllPairs.drop⁺

      take⁺ : ∀ {n} m {xs} → Unique S {m + n} xs → Unique S {m} (take m xs)
      take⁺ = AllPairs.take⁺

    ------------------------------------------------------------------------
    -- tabulate

    module _ (S : Setoid a ℓ) where

      open Setoid S renaming (Carrier to A)

      tabulate⁺ : ∀ {n} {f : Fin n → A} → (∀ {i j} → f i ≈ f j → i ≡ j) →
                  Unique S (tabulate f)
      tabulate⁺ f-inj = AllPairs.tabulate⁺ (_∘ f-inj)

    ------------------------------------------------------------------------
    -- lookup

    module _ (S : Setoid a ℓ) where

      open Setoid S

      lookup-injective : ∀ {n xs} → Unique S {n} xs → ∀ i j → lookup xs i ≈ lookup xs j → i ≡ j
      lookup-injective (px ∷ pxs) zero zero eq = ≡.refl
      lookup-injective (px ∷ pxs) zero (suc j) eq = contradiction eq (All.lookup⁺ px j)
      lookup-injective (px ∷ pxs) (suc i) zero eq = contradiction (sym eq) (All.lookup⁺ px i)
      lookup-injective (px ∷ pxs) (suc i) (suc j) eq = ≡.cong suc (lookup-injective pxs i j eq)