------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of unique lists (setoid equality) using K
------------------------------------------------------------------------
 
{-# OPTIONS --safe --with-K #-}
 
module Data.List.Relation.Unary.Unique.Propositional.Properties.WithK where
 
open import Data.Empty
open import Data.List using (List)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.BagAndSetEquality
open import Data.List.Relation.Unary.All.Properties
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.Unique.Propositional
open import Data.Product
open import Function.Bundles
open import Level using (Level)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
 
private
  variable
    a : Level
    A : Set a
    l l' : List A
 
------------------------------------------------------------------------
-- membership
 
unique⇒∈-prop : Unique l → (x : A) → Irrelevant (x ∈ l)
unique⇒∈-prop (hx ∷ h) x (here refl) (here refl) = refl
unique⇒∈-prop (hx ∷ h) x (here refl) (there b)   = ⊥-elim (All¬⇒¬Any hx b)
unique⇒∈-prop (hx ∷ h) x (there a)   (here refl) = ⊥-elim (All¬⇒¬Any hx a)
unique⇒∈-prop (hx ∷ h) x (there a)   (there b) rewrite unique⇒∈-prop h x a b = refl
 
unique∧set⇒bag : Unique l → Unique l' → l ∼[ set ] l' → l ∼[ bag ] l'
unique∧set⇒bag h h' eq {a} = record
  { to = to
  ; from = from
  ; to-cong = to-cong
  ; from-cong = from-cong
  ; inverse = (λ {x} {y} _ → unique⇒∈-prop h' a (to y) x)
            , (λ {x} {y} _ → unique⇒∈-prop h a (from y) x)
  }
  where open Equivalence (eq {a})