------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise decidable equality over lists parameterised by a setoid
------------------------------------------------------------------------

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

open import Relation.Binary.Bundles using (DecSetoid)

module Data.List.Relation.Binary.Equality.DecSetoid
  {a ℓ} (DS : DecSetoid a ℓ) where

import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
open import Data.List.Relation.Binary.Pointwise using (decSetoid)
open DecSetoid DS using (setoid)

------------------------------------------------------------------------
-- Additional properties

≋-decSetoid : DecSetoid _ _
≋-decSetoid = decSetoid DS

open DecSetoid ≋-decSetoid public
  using ()
  renaming (isDecEquivalence to ≋-isDecEquivalence; _≟_ to _≋?_)

------------------------------------------------------------------------
-- Make all definitions from setoid equality available

open SetoidEquality setoid public