    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Equality over container extensions parametrised by some setoid
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (Setoid)

    module Data.Container.Relation.Binary.Equality.Setoid {c e} (S : Setoid c e) where

    open import Level using (_⊔_; suc)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Structures using (IsEquivalence)
    open import Relation.Binary.Definitions
      using (Reflexive; Symmetric; Transitive)
    open import Data.Container.Core using (Container; ⟦_⟧)
    open import Data.Container.Relation.Binary.Pointwise using (Pointwise)
    import Data.Container.Relation.Binary.Pointwise.Properties as Pw

    private
      module S = Setoid S
    open S using (_≈_) renaming (Carrier to X)

    ------------------------------------------------------------------------
    -- Definition of equality

    module _ {s p} (C : Container s p) where

      Eq : Rel (⟦ C ⟧ X) (e ⊔ s ⊔ p)
      Eq = Pointwise C _≈_

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

      refl : Reflexive Eq
      refl = Pw.refl C _ S.refl

      sym : Symmetric Eq
      sym = Pw.sym C _ S.sym

      trans : Transitive Eq
      trans = Pw.trans C _ S.trans

      isEquivalence : IsEquivalence Eq
      isEquivalence = record
        { refl  = refl
        ; sym   = sym
        ; trans = trans
        }

      setoid : Setoid (s ⊔ p ⊔ c) (s ⊔ p ⊔ e)
      setoid = record
        { isEquivalence = isEquivalence
        }