------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to propositional list membership, that rely on
-- the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.List.Membership.Propositional.Properties.WithK where

open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
open import Data.List.Membership.Propositional using (_∈_; _∉_)
import Data.List.Membership.Setoid.Properties as Membership
  using (unique⇒irrelevant)
open import Data.List.Relation.Binary.BagAndSetEquality using (_∼[_]_; set; bag)
open import Data.Product using (_,_)
open import Function.Bundles using (Equivalence)
open import Level using (Level)
open import Relation.Unary using (Irrelevant)
open import Relation.Binary.PropositionalEquality.Properties as ≡
open import Relation.Binary.PropositionalEquality.WithK using (≡-irrelevant)

private
  variable
    a : Level
    A : Set a
    xs ys : List A

------------------------------------------------------------------------
-- Irrelevance

unique⇒irrelevant : Unique xs → Irrelevant (_∈ xs)
unique⇒irrelevant = Membership.unique⇒irrelevant (≡.setoid _) ≡-irrelevant

unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
unique∧set⇒bag p p′ eq = record
  { Equivalence eq
  ; inverse = (λ _ → unique⇒irrelevant p′ _ _) , (λ _ → unique⇒irrelevant p _ _) }