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

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

open import Relation.Binary.Bundles using (DecSetoid)
open import Relation.Binary.Structures using (IsDecEquivalence)
open import Relation.Binary.Definitions using (Decidable)

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

import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Pointwise as PW
open import Level
open import Relation.Binary.Definitions using (Decidable)
open DecSetoid DS

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

open SetoidEquality setoid public

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

infix  _≋?_

_≋?_ : Decidable _≋_
_≋?_ = PW.decidable _≟_

≋-isDecEquivalence : IsDecEquivalence _≋_
≋-isDecEquivalence = PW.isDecEquivalence isDecEquivalence

≋-decSetoid : DecSetoid a (a ⊔ ℓ)
≋-decSetoid = PW.decSetoid DS