```------------------------------------------------------------------------
-- Alternative definition of bag and set equality
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Data.Container.AlternativeBagAndSetEquality where

open import Data.Container
open import Data.Product as Prod
open import Function
open import Function.Equality using (_⟨\$⟩_)
open import Function.Equivalence as Eq using (_⇔_; module Equivalent)
open import Function.Inverse as Inv using (Isomorphism; module Inverse)
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

open P.≡-Reasoning

-- Another way to define bag and set equality. Two containers xs and
-- ys are equal when viewed as bags if their sets of positions are
-- equipotent and the position functions map related positions to
-- equal values. For set equality the position sets do not need to be
-- equipotent, only equiinhabited.

infix 4 _≈[_]′_

_≈[_]′_ : ∀ {c} {C : Container c} {X : Set c} →
⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set c
_≈[_]′_ {C = C} (s , f) k (s′ , f′) =
∃ λ (p₁≈p₂ : Isomorphism k (Position C s) (Position C s′)) →
(∀ p → f  p ≡ f′ (Equivalent.to   (Inv.⇒⇔ p₁≈p₂) ⟨\$⟩ p)) ×
(∀ p → f′ p ≡ f  (Equivalent.from (Inv.⇒⇔ p₁≈p₂) ⟨\$⟩ p))
-- The last component is unnecessary when k equals bag.

-- This definition is equivalent to the one in Data.Container.

private

≈⇔≈′-set : ∀ {c} {C : Container c} {X : Set c} (xs ys : ⟦ C ⟧ X) →
xs ≈[ set ] ys ⇔ xs ≈[ set ]′ ys
≈⇔≈′-set {c} xs ys = Eq.equivalent to from
where
to : xs ≈[ set ] ys → xs ≈[ set ]′ ys
to xs≈ys =
Eq.equivalent
(λ p → proj₁ \$ Equivalent.to   xs≈ys ⟨\$⟩ (p , refl))
(λ p → proj₁ \$ Equivalent.from xs≈ys ⟨\$⟩ (p , refl)) ,
(λ p → proj₂ (Equivalent.to   xs≈ys ⟨\$⟩ (p , refl))) ,
(λ p → proj₂ (Equivalent.from xs≈ys ⟨\$⟩ (p , refl)))

from : xs ≈[ set ]′ ys → xs ≈[ set ] ys
from (p₁≈p₂ , f₁≈f₂ , f₂≈f₁) {z} =
Eq.equivalent
(Prod.map (_⟨\$⟩_ (Equivalent.to p₁≈p₂))
(λ {x} eq → begin
z                                     ≡⟨ eq ⟩
proj₂ xs x                            ≡⟨ f₁≈f₂ x ⟩
proj₂ ys (Equivalent.to p₁≈p₂ ⟨\$⟩ x)  ∎))
(Prod.map (_⟨\$⟩_ (Equivalent.from p₁≈p₂))
(λ {x} eq → begin
z                                       ≡⟨ eq ⟩
proj₂ ys x                              ≡⟨ f₂≈f₁ x ⟩
proj₂ xs (Equivalent.from p₁≈p₂ ⟨\$⟩ x)  ∎))

≈⇔≈′-bag : ∀ {c} {C : Container c} {X : Set c} (xs ys : ⟦ C ⟧ X) →
xs ≈[ bag ] ys ⇔ xs ≈[ bag ]′ ys
≈⇔≈′-bag {c} {C} {X} xs ys = Eq.equivalent t f
where
open Inverse

t : xs ≈[ bag ] ys → xs ≈[ bag ]′ ys
t xs≈ys =
record { to         = Equivalent.to   (proj₁ xs∼ys)
; from       = Equivalent.from (proj₁ xs∼ys)
; inverse-of = record
{ left-inverse-of  = from∘to
; right-inverse-of = to∘from
}
} ,
proj₂ xs∼ys
where
xs∼ys = Equivalent.to (≈⇔≈′-set xs ys) ⟨\$⟩ Inv.⇿⇒ xs≈ys

from∘to : ∀ p → proj₁ (from xs≈ys ⟨\$⟩
(proj₁ (to xs≈ys ⟨\$⟩ (p , refl)) ,
refl)) ≡ p
from∘to p = begin
proj₁ (from xs≈ys ⟨\$⟩ (proj₁ (to xs≈ys ⟨\$⟩ (p , refl)) , refl))  ≡⟨ lemma (to xs≈ys ⟨\$⟩ (p , refl)) ⟩
proj₁ (from xs≈ys ⟨\$⟩        (to xs≈ys ⟨\$⟩ (p , refl))        )  ≡⟨ P.cong proj₁ \$
left-inverse-of xs≈ys (p , refl) ⟩
p                                                                ∎
where
lemma : ∀ {y} (x : ∃ λ p′ → y ≡ proj₂ ys p′) →
proj₁ (from xs≈ys ⟨\$⟩ (proj₁ x , refl)) ≡
proj₁ (from xs≈ys ⟨\$⟩        x        )
lemma (p′ , refl) = refl

to∘from : ∀ p → proj₁ (to xs≈ys ⟨\$⟩
(proj₁ (from xs≈ys ⟨\$⟩ (p , refl)) ,
refl)) ≡ p
to∘from p = begin
proj₁ (to xs≈ys ⟨\$⟩ (proj₁ (from xs≈ys ⟨\$⟩ (p , refl)) , refl))  ≡⟨ lemma (from xs≈ys ⟨\$⟩ (p , refl)) ⟩
proj₁ (to xs≈ys ⟨\$⟩        (from xs≈ys ⟨\$⟩ (p , refl))        )  ≡⟨ P.cong proj₁ \$
right-inverse-of xs≈ys (p , refl) ⟩
p                                                                ∎
where
lemma : ∀ {y} (x : ∃ λ p′ → y ≡ proj₂ xs p′) →
proj₁ (to xs≈ys ⟨\$⟩ (proj₁ x , refl)) ≡
proj₁ (to xs≈ys ⟨\$⟩        x        )
lemma (p′ , refl) = refl

f : xs ≈[ bag ]′ ys → xs ≈[ bag ] ys
f (p₁≈p₂ , f₁≈f₂ , f₂≈f₁) {z} = record
{ to         = Equivalent.to   xs∼ys
; from       = Equivalent.from xs∼ys
; inverse-of = record
{ left-inverse-of  = λ x →
let eq = P.trans (P.trans (proj₂ x) (P.trans (f₁≈f₂ (proj₁ x)) refl))
(P.trans (f₂≈f₁ (to p₁≈p₂ ⟨\$⟩ proj₁ x)) refl) in
H.≅-to-≡ \$
H.cong₂ {B = λ x → z ≡ proj₂ xs x}
_,_ (H.≡-to-≅ \$ left-inverse-of  p₁≈p₂ (proj₁ x))
(proof-irrelevance eq (proj₂ x))
; right-inverse-of = λ x →
let eq = P.trans (P.trans (proj₂ x) (P.trans (f₂≈f₁ (proj₁ x)) refl))
(P.trans (f₁≈f₂ (from p₁≈p₂ ⟨\$⟩ proj₁ x)) refl) in
H.≅-to-≡ \$
H.cong₂ {B = λ x → z ≡ proj₂ ys x}
_,_ (H.≡-to-≅ \$ right-inverse-of p₁≈p₂ (proj₁ x))
(proof-irrelevance eq (proj₂ x))
}
}
where
xs∼ys = Equivalent.from (≈⇔≈′-set xs ys) ⟨\$⟩
(Inv.⇿⇒ p₁≈p₂ , f₁≈f₂ , f₂≈f₁)

proof-irrelevance : {A : Set c} {x y z : A}
(p : x ≡ y) (q : x ≡ z) → p ≅ q
proof-irrelevance refl refl = refl

≈⇔≈′ : ∀ {k c} {C : Container c} {X : Set c} (xs ys : ⟦ C ⟧ X) →
xs ≈[ k ] ys ⇔ xs ≈[ k ]′ ys
≈⇔≈′ {set} = ≈⇔≈′-set
≈⇔≈′ {bag} = ≈⇔≈′-bag
```