1 files changed, 131 insertions, 0 deletions
diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda
new file mode 100644
index 0000000..99501d6
--- /dev/null
+++ b/Data/Opaque/Multiset.agda
@@ -0,0 +1,131 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
+
+module Data.Opaque.Multiset where
+
+import Data.List as L
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
+import Data.Opaque.List as List
+
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Data.List.Effectful.Foldable using (foldable; ++-homo)
+open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; ↭-refl)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺; ++⁺; ++-comm)
+open import Algebra.Morphism using (IsMonoidHomomorphism)
+open import Data.Product using (_,_; uncurry′)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Effect.Foldable using (RawFoldable)
+open import Function using (_⟶ₛ_; Func; _⟨$⟩_; id)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Setoid)
+
+open Func
+
+private
+
+  variable
+    a c ℓ : Level
+    A B : Set a
+    Aₛ Bₛ : Setoid c ℓ
+
+opaque
+
+  Multiset : Set a → Set a
+  Multiset = L.List
+
+  [] : Multiset A
+  [] = L.[]
+
+  _∷_ : A → Multiset A → Multiset A
+  _∷_ = L._∷_
+
+  map : (A → B) → Multiset A → Multiset B
+  map = L.map
+
+  _++_ : Multiset A → Multiset A → Multiset A
+  _++_ = L._++_
+
+  Multisetₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ)
+  Multisetₛ = ↭-setoid
+
+  []ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Multisetₛ {c} {ℓ} Aₛ
+  []ₛ {Aₛ} = Const ⊤ₛ (Multisetₛ Aₛ) []
+
+  ∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ
+  ∷ₛ .to = uncurry′ _∷_
+  ∷ₛ .cong = uncurry′ ↭.prep
+
+  [-]ₛ : Aₛ ⟶ₛ Multisetₛ Aₛ
+  [-]ₛ .to = L.[_]
+  [-]ₛ {Aₛ} .cong y = ↭.prep y (↭-refl Aₛ)
+
+  mapₛ : (Aₛ ⟶ₛ Bₛ) → Multisetₛ Aₛ ⟶ₛ Multisetₛ Bₛ
+  mapₛ f .to = map (to f)
+  mapₛ {Aₛ} {Bₛ} f .cong xs≈ys = map⁺ Aₛ Bₛ (cong f) xs≈ys
+
+  ++ₛ : Multisetₛ Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ
+  ++ₛ .to = uncurry′ _++_
+  ++ₛ {Aₛ} .cong = uncurry′ (++⁺ Aₛ)
+
+  ++ₛ-comm
+      : (open Setoid (Multisetₛ Aₛ))
+      → (xs ys : Carrier)
+      → ++ₛ ⟨$⟩ (xs , ys) ≈ ++ₛ ⟨$⟩ (ys , xs)
+  ++ₛ-comm {Aₛ} xs ys = ++-comm Aₛ xs ys
+
+module _ (M : CommutativeMonoid c ℓ) where
+
+  open CommutativeMonoid M renaming (setoid to Mₛ)
+
+  opaque
+    unfolding Multiset List.fold-cong
+    fold : ∣ Multisetₛ Mₛ ∣ → ∣ Mₛ ∣
+    fold = List.fold monoid -- RawFoldable.fold foldable rawMonoid
+
+    fold-cong
+        : {xs ys : ∣ Multisetₛ Mₛ ∣}
+        → (let module [M]ₛ = Setoid (Multisetₛ Mₛ))
+        → (xs [M]ₛ.≈ ys)
+        → fold xs ≈ fold ys
+    fold-cong (↭.refl x) = cong (List.foldₛ monoid) x
+    fold-cong (↭.prep x≈y xs↭ys) = ∙-cong x≈y (fold-cong xs↭ys)
+    fold-cong
+        {x₀ L.∷ x₁ L.∷ xs}
+        {y₀ L.∷ y₁ L.∷ ys}
+        (↭.swap x₀≈y₁ x₁≈y₀ xs↭ys) = trans
+            (sym (assoc x₀ x₁ (fold xs))) (trans 
+            (∙-cong (trans (∙-cong x₀≈y₁ x₁≈y₀) (comm y₁ y₀)) (fold-cong xs↭ys))
+            (assoc y₀ y₁ (fold ys)))
+    fold-cong {xs} {ys} (↭.trans xs↭zs zs↭ys) = trans (fold-cong xs↭zs) (fold-cong zs↭ys)
+
+  foldₛ : Multisetₛ Mₛ ⟶ₛ Mₛ
+  foldₛ .to = fold
+  foldₛ .cong = fold-cong
+
+  opaque
+    unfolding fold
+    ++ₛ-homo
+        : (xs ys : ∣ Multisetₛ Mₛ ∣)
+        → foldₛ ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys)) ≈ (foldₛ ⟨$⟩ xs) ∙ (foldₛ ⟨$⟩ ys)
+    ++ₛ-homo xs ys = ++-homo monoid id xs
+
+    []ₛ-homo : foldₛ ⟨$⟩ ([]ₛ ⟨$⟩ _) ≈ ε
+    []ₛ-homo = refl
+
+module _ (M N : CommutativeMonoid c ℓ) where
+
+  module M = CommutativeMonoid M
+  module N = CommutativeMonoid N
+
+  opaque
+    unfolding fold
+
+    fold-mapₛ
+        : (f : M.setoid ⟶ₛ N.setoid)
+        → IsMonoidHomomorphism M.rawMonoid N.rawMonoid (to f)
+        → {xs : ∣ Multisetₛ M.setoid ∣}
+        → foldₛ N ⟨$⟩ (mapₛ f ⟨$⟩ xs) N.≈ f ⟨$⟩ (foldₛ M ⟨$⟩ xs)
+    fold-mapₛ = List.fold-mapₛ M.monoid N.monoid