Add free commutative monoid functor

7 files changed, 257 insertions, 121 deletions

diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda
new file mode 100644
index 0000000..2ba0a0e
--- /dev/null
+++ b/Data/Opaque/Multiset.agda
@@ -0,0 +1,67 @@
+{-# OPTIONS --without-K --safe #-}
+{-# OPTIONS --hidden-argument-puns #-}
+
+module Data.Opaque.Multiset where
+
+import Data.List as L
+
+open import Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; prep)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺; ++⁺; ++-comm)
+open import Data.Product using (_,_)
+open import Data.Product using (uncurry′)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Function using (_⟶ₛ_; Func; _⟨$⟩_)
+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
+
+  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
diff --git a/Functor/Free/Instance/CMonoid.agda b/Functor/Free/Instance/CMonoid.agda
new file mode 100644
index 0000000..be9cb94
--- /dev/null
+++ b/Functor/Free/Instance/CMonoid.agda
@@ -0,0 +1,116 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_)
+
+module Functor.Free.Instance.CMonoid {c ℓ : Level} where
+
+import Categories.Object.Monoid as MonoidObject
+import Object.Monoid.Commutative as CMonoidObject
+
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor)
+open import Categories.NaturalTransformation using (NaturalTransformation)
+open import Category.Construction.CMonoids using (CMonoids)
+open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×; ×-symmetric′)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (++-assoc; ++-identityˡ; ++-identityʳ; ++-comm)
+open import Data.Product using (_,_)
+open import Data.Setoid using (∣_∣)
+open import Data.Opaque.Multiset using ([]ₛ; Multisetₛ; ++ₛ; mapₛ)
+open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
+open import NaturalTransformation.Instance.EmptyMultiset {c} {ℓ} using (⊤⇒[])
+open import NaturalTransformation.Instance.MultisetAppend {c} {ℓ} using (++)
+open import Relation.Binary using (Setoid)
+
+module ++ = NaturalTransformation ++
+module ⊤⇒[] = NaturalTransformation ⊤⇒[]
+
+open Functor
+open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒)
+open CMonoidObject Setoids-×.symmetric using (CommutativeMonoid; IsCommutativeMonoid; CommutativeMonoid⇒)
+open IsCommutativeMonoid
+open CommutativeMonoid using () renaming (μ to μ′; η to η′)
+open IsMonoid
+open CommutativeMonoid⇒
+open Monoid⇒
+
+module _ (X : Setoid c ℓ) where
+
+  open Setoid (Multiset.₀ X)
+
+  opaque
+
+    unfolding Multisetₛ
+
+    ++ₛ-assoc
+        : (x y z : ∣ Multisetₛ X ∣)
+        → ++ₛ ⟨$⟩ (++ₛ ⟨$⟩ (x , y) , z)
+        ≈ ++ₛ ⟨$⟩ (x , ++ₛ ⟨$⟩ (y , z))
+    ++ₛ-assoc x y z = ++-assoc X x y z
+
+    ++ₛ-identityˡ
+        : (x : ∣ Multisetₛ X ∣)
+        → x ≈ ++ₛ ⟨$⟩ ([]ₛ ⟨$⟩ _ , x)
+    ++ₛ-identityˡ x = ++-identityˡ X x
+
+    ++ₛ-identityʳ
+        : (x : ∣ Multisetₛ X ∣)
+        → x ≈ ++ₛ ⟨$⟩ (x , []ₛ ⟨$⟩ _)
+    ++ₛ-identityʳ x = sym (++-identityʳ X x)
+
+    ++ₛ-comm
+        : (x y : ∣ Multisetₛ X ∣)
+        → ++ₛ ⟨$⟩ (x , y) ≈ ++ₛ ⟨$⟩ (y , x)
+    ++ₛ-comm x y = ++-comm X x y
+
+  opaque
+    unfolding ×-symmetric′
+    MultisetCMonoid : IsCommutativeMonoid (Multiset.₀ X)
+    MultisetCMonoid .isMonoid .μ = ++.η X
+    MultisetCMonoid .isMonoid .η = ⊤⇒[].η X
+    MultisetCMonoid .isMonoid .assoc {(x , y) , z} = ++ₛ-assoc x y z
+    MultisetCMonoid .isMonoid .identityˡ {_ , x} = ++ₛ-identityˡ x
+    MultisetCMonoid .isMonoid .identityʳ {x , _} = ++ₛ-identityʳ x
+    MultisetCMonoid .commutative {x , y} = ++ₛ-comm x y
+
+Multisetₘ : (X : Setoid c ℓ) → CommutativeMonoid
+Multisetₘ X = record { isCommutativeMonoid = MultisetCMonoid X }
+
+open Setoids-× using (_⊗₀_; _⊗₁_)
+opaque
+  unfolding MultisetCMonoid
+  mapₛ-++ₛ
+      : {A B : Setoid c ℓ}
+      → (f : A ⟶ₛ B)
+      → {xy : ∣ Multisetₛ A ⊗₀ Multisetₛ A ∣}
+      → (open Setoid (Multisetₛ B))
+      → mapₛ f ⟨$⟩ (μ′ (Multisetₘ A) ⟨$⟩ xy)
+      ≈ μ′ (Multisetₘ B) ⟨$⟩ (mapₛ f ⊗₁ mapₛ f ⟨$⟩ xy)
+  mapₛ-++ₛ = ++.sym-commute
+
+opaque
+  unfolding MultisetCMonoid mapₛ
+  mapₛ-[]ₛ
+      : {A B : Setoid c ℓ}
+      → (f : A ⟶ₛ B)
+      → {x : ∣ Setoids-×.unit ∣}
+      → (open Setoid (Multisetₛ B))
+      → mapₛ f ⟨$⟩ (η′ (Multisetₘ A) ⟨$⟩ x)
+      ≈ η′ (Multisetₘ B) ⟨$⟩ x
+  mapₛ-[]ₛ = ⊤⇒[].commute
+
+mapₘ
+    : {A B : Setoid c ℓ}
+      (f : A ⟶ₛ B)
+    → CommutativeMonoid⇒ (Multisetₘ A) (Multisetₘ B)
+mapₘ f .monoid⇒ .arr = Multiset.₁ f
+mapₘ f .monoid⇒ .preserves-μ = mapₛ-++ₛ f
+mapₘ f .monoid⇒ .preserves-η = mapₛ-[]ₛ f
+
+Free : Functor (Setoids c ℓ) (CMonoids Setoids-×.symmetric)
+Free .F₀ = Multisetₘ
+Free .F₁ = mapₘ
+Free .identity {X} = Multiset.identity {X}
+Free .homomorphism {X} {Y} {Z} {f} {g} = Multiset.homomorphism {X} {Y} {Z} {f} {g}
+Free .F-resp-≈ {A} {B} {f} {g} = Multiset.F-resp-≈ {A} {B} {f} {g}
diff --git a/Functor/Free/Instance/Monoid.agda b/Functor/Free/Instance/Monoid.agda
index e08e42d..c8450b9 100644
--- a/Functor/Free/Instance/Monoid.agda
+++ b/Functor/Free/Instance/Monoid.agda
@@ -24,8 +24,6 @@ open import NaturalTransformation.Instance.ListAppend {c} {ℓ} using (++)
 open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-
 module ++ = NaturalTransformation ++
 module ⊤⇒[] = NaturalTransformation ⊤⇒[]
 
diff --git a/Functor/Instance/FreeCMonoid.agda b/Functor/Instance/FreeCMonoid.agda
deleted file mode 100644
index 1b241b7..0000000
--- a/Functor/Instance/FreeCMonoid.agda
+++ /dev/null
@@ -1,67 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Level using (Level; _⊔_)
-
-module Functor.Instance.FreeCMonoid {c ℓ : Level} where
-
-import Categories.Object.Monoid as MonoidObject
-import Object.Monoid.Commutative as CMonoidObject
-
-open import Categories.Category.Instance.Setoids using (Setoids)
-open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
-open import Categories.Functor using (Functor)
-open import Categories.NaturalTransformation using (NaturalTransformation)
-open import Category.Construction.CMonoids using (CMonoids)
-open import Category.Instance.Setoids.SymmetricMonoidal {c} {c ⊔ ℓ} using (Setoids-×)
-open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (++-assoc; ++-identityˡ; ++-identityʳ; ++-comm)
-open import Data.Product using (_,_)
-open import Function using (_⟶ₛ_)
-open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
-open import NaturalTransformation.Instance.EmptyMultiset {c} {ℓ} using (⊤⇒[])
-open import NaturalTransformation.Instance.MultisetAppend {c} {ℓ} using (++)
-open import Relation.Binary using (Setoid)
-
-module Multiset = Functor Multiset
-module Setoids-× = SymmetricMonoidalCategory Setoids-×
-module ++ = NaturalTransformation ++
-module ⊤⇒[] = NaturalTransformation ⊤⇒[]
-
-open Functor
-open MonoidObject Setoids-×.monoidal using (Monoid; IsMonoid; Monoid⇒)
-open CMonoidObject Setoids-×.symmetric using (CommutativeMonoid; IsCommutativeMonoid; CommutativeMonoid⇒)
-open IsCommutativeMonoid
-open IsMonoid
-open CommutativeMonoid⇒
-open Monoid⇒
-
-module _ (X : Setoid c ℓ) where
-
-  private
-    module X = Setoid X
-    module MultisetX = Setoid (Multiset.₀ X)
-
-  MultisetCMonoid : IsCommutativeMonoid (Multiset.₀ X)
-  MultisetCMonoid .isMonoid .μ = ++.η X
-  MultisetCMonoid .isMonoid .η = ⊤⇒[].η X
-  MultisetCMonoid .isMonoid .assoc {(x , y) , z} = ++-assoc X x y z
-  MultisetCMonoid .isMonoid .identityˡ {_ , x} = ++-identityˡ X x
-  MultisetCMonoid .isMonoid .identityʳ {x , _} = MultisetX.sym (++-identityʳ X x)
-  MultisetCMonoid .commutative {x , y} = ++-comm X x y
-
-FreeCMonoid₀ : (X : Setoid c ℓ) → CommutativeMonoid
-FreeCMonoid₀ X = record { isCommutativeMonoid = MultisetCMonoid X }
-
-FreeCMonoid₁
-    : {A B : Setoid c ℓ}
-      (f : A ⟶ₛ B)
-    → CommutativeMonoid⇒ (FreeCMonoid₀ A) (FreeCMonoid₀ B)
-FreeCMonoid₁ f .monoid⇒ .arr = Multiset.₁ f
-FreeCMonoid₁ f .monoid⇒ .preserves-μ {xy} = ++.sym-commute f {xy}
-FreeCMonoid₁ f .monoid⇒ .preserves-η = ⊤⇒[].commute f
-
-FreeCMonoid : Functor (Setoids c ℓ) (CMonoids Setoids-×.symmetric)
-FreeCMonoid .F₀ = FreeCMonoid₀
-FreeCMonoid .F₁ = FreeCMonoid₁
-FreeCMonoid .identity {X} = Multiset.identity {X}
-FreeCMonoid .homomorphism {X} {Y} {Z} {f} {g} = Multiset.homomorphism {X} {Y} {Z} {f} {g}
-FreeCMonoid .F-resp-≈ {A} {B} {f} {g} = Multiset.F-resp-≈ {A} {B} {f} {g}
diff --git a/Functor/Instance/Multiset.agda b/Functor/Instance/Multiset.agda
index 0adb1df..b961c7b 100644
--- a/Functor/Instance/Multiset.agda
+++ b/Functor/Instance/Multiset.agda
@@ -4,18 +4,20 @@ open import Level using (Level; _⊔_)
 
 module Functor.Instance.Multiset {c ℓ : Level} where
 
-import Data.List as List
+import Data.Opaque.List as L
 import Data.List.Properties as ListProps
 import Data.List.Relation.Binary.Pointwise as PW
 
-open import Data.List.Relation.Binary.Permutation.Setoid using (↭-setoid; ↭-reflexive-≋)
-open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺)
-
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor)
-open import Data.Setoid using (∣_∣)
+open import Data.List.Relation.Binary.Permutation.Setoid using (↭-setoid; ↭-reflexive-≋)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺)
+open import Data.Opaque.Multiset using (Multisetₛ; mapₛ)
+open import Data.Setoid using (∣_∣; _⇒ₛ_)
 open import Function.Base using (_∘_; id)
 open import Function.Bundles using (Func; _⟶ₛ_; _⟨$⟩_)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Function.Construct.Setoid using (_∙_)
 open import Relation.Binary using (Setoid)
 
 open Functor
@@ -29,32 +31,42 @@ private
 -- the Multiset functor takes a carrier A to lists of A
 -- and the equivalence on A to permutation equivalence on lists of A
 
-Multisetₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ)
-Multisetₛ x = ↭-setoid x
-
 -- Multiset on morphisms applies the same function to every element of a multiset
 
-mapₛ : A ⟶ₛ B → Multisetₛ A ⟶ₛ Multisetₛ B
-mapₛ f .to = List.map (to f)
-mapₛ {A} {B} f .cong = map⁺ A B (cong f)
+opaque
+  unfolding mapₛ
+
+  map-id
+      : (xs : ∣ Multisetₛ A ∣)
+      → (open Setoid (Multisetₛ A))
+      → mapₛ (Id A) ⟨$⟩ xs ≈ xs
+  map-id {A} = reflexive (Multisetₛ A) ∘ ListProps.map-id
+
+opaque
+  unfolding mapₛ
 
-map-id
-    : (xs : ∣ Multisetₛ A ∣)
-    → (open Setoid (Multisetₛ A))
-    → List.map id xs ≈ xs
-map-id {A} = reflexive (Multisetₛ A) ∘ ListProps.map-id
+  Multiset-homo
+      : (f : A ⟶ₛ B)
+        (g : B ⟶ₛ C)
+      → (xs : ∣ Multisetₛ A ∣)
+      → (open Setoid (Multisetₛ C))
+      → mapₛ (g ∙ f) ⟨$⟩ xs ≈ mapₛ g ⟨$⟩ (mapₛ f ⟨$⟩ xs)
+  Multiset-homo {C = C} f g = reflexive (Multisetₛ C) ∘ ListProps.map-∘
 
-Multiset-homo
-    : (f : A ⟶ₛ B)
-      (g : B ⟶ₛ C)
-    → (xs : ∣ Multisetₛ A ∣)
-    → (open Setoid (Multisetₛ C))
-    → List.map (to g ∘ to f) xs ≈ List.map (to g) (List.map (to f) xs)
-Multiset-homo {C = C} f g = reflexive (Multisetₛ C) ∘ ListProps.map-∘
+opaque
+  unfolding mapₛ
+
+  Multiset-resp-≈
+      : (f g : A ⟶ₛ B)
+      → (let open Setoid (A ⇒ₛ B) in f ≈ g)
+      → (let open Setoid (Multisetₛ A ⇒ₛ Multisetₛ B) in mapₛ f ≈ mapₛ g)
+  Multiset-resp-≈ {A} {B} f g f≈g = ↭-reflexive-≋ B (PW.map⁺ (to f) (to g) (PW.refl f≈g))
 
 Multiset : Functor (Setoids c ℓ) (Setoids c (c ⊔ ℓ))
 Multiset .F₀ = Multisetₛ
 Multiset .F₁ = mapₛ
 Multiset .identity {A} {xs} = map-id {A} xs
 Multiset .homomorphism {f = f} {g} {xs} = Multiset-homo f g xs
-Multiset .F-resp-≈ {A} {B} {f} {g} f≈g = ↭-reflexive-≋ B (PW.map⁺ (to f) (to g) (PW.refl f≈g))
+Multiset .F-resp-≈ {A} {B} {f} {g} f≈g = Multiset-resp-≈ f g f≈g
+
+module Multiset = Functor Multiset
diff --git a/NaturalTransformation/Instance/EmptyMultiset.agda b/NaturalTransformation/Instance/EmptyMultiset.agda
index 9c3a779..bfec451 100644
--- a/NaturalTransformation/Instance/EmptyMultiset.agda
+++ b/NaturalTransformation/Instance/EmptyMultiset.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level)
+open import Level using (Level; _⊔_)
 
 module NaturalTransformation.Instance.EmptyMultiset {c ℓ : Level} where
 
@@ -8,16 +8,27 @@ import Function.Construct.Constant as Const
 
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.Functor using (Functor)
-open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
+open import Data.Setoid.Unit {c} {c ⊔ ℓ} using (⊤ₛ)
 open import Categories.Functor.Construction.Constant using (const)
-open import Data.List using ([])
+open import Data.Opaque.Multiset using (Multisetₛ; []ₛ; mapₛ)
 open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
+open import Function.Construct.Constant using () renaming (function to Const)
 open import Relation.Binary using (Setoid)
+open import Data.Setoid using (_⇒ₛ_)
+open import Function using (Func; _⟶ₛ_)
+open import Function.Construct.Setoid using (_∙_)
 
-module Multiset = Functor Multiset
+opaque
+  unfolding mapₛ
+  map-[]ₛ
+      : {A B : Setoid c ℓ}
+      → (f : A ⟶ₛ B)
+      → (open Setoid (⊤ₛ ⇒ₛ Multisetₛ B))
+      → []ₛ ≈ mapₛ f ∙ []ₛ
+  map-[]ₛ {B = B} f = Setoid.refl (Multisetₛ B)
 
-⊤⇒[] : NaturalTransformation (const SingletonSetoid) Multiset
+⊤⇒[] : NaturalTransformation (const ⊤ₛ) Multiset
 ⊤⇒[] = ntHelper record
-    { η = λ X → Const.function SingletonSetoid (Multiset.₀ X) []
-    ; commute = λ {_} {B} f → Setoid.refl (Multiset.₀ B)
+    { η = λ X → []ₛ {Aₛ = X}
+    ; commute = map-[]ₛ
     }
diff --git a/NaturalTransformation/Instance/MultisetAppend.agda b/NaturalTransformation/Instance/MultisetAppend.agda
index b0e8bc4..f786124 100644
--- a/NaturalTransformation/Instance/MultisetAppend.agda
+++ b/NaturalTransformation/Instance/MultisetAppend.agda
@@ -4,43 +4,42 @@ open import Level using (Level; _⊔_)
 
 module NaturalTransformation.Instance.MultisetAppend {c ℓ : Level} where
 
-open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
-open import Categories.Category.Product using (_※_)
+import Data.Opaque.List as L
+
 open import Categories.Category.BinaryProducts using (module BinaryProducts)
-open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
 open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cartesian)
+open import Categories.Category.Product using (_※_)
 open import Categories.Functor using (Functor; _∘F_)
-open import Data.List using (List; _++_; map)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Data.List.Properties using (map-++)
 open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (++⁺)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Opaque.Multiset using (Multisetₛ; mapₛ; ++ₛ)
 open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_)
 open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
-open import Function using (Func; _⟶ₛ_)
 open import Relation.Binary using (Setoid)
 
-module Multiset = Functor Multiset
-
 open Cartesian (Setoids-Cartesian {c} {c ⊔ ℓ}) using (products)
 open BinaryProducts products using (-×-)
 open Func
 
-++ₛ : {X : Setoid c ℓ} → Multiset.₀ X ×ₛ Multiset.₀ X ⟶ₛ Multiset.₀ X
-++ₛ .to (xs , ys) = xs ++ ys
-++ₛ {A} .cong (≈xs , ≈ys) = ++⁺ A ≈xs ≈ys
+opaque
+  unfolding ++ₛ mapₛ
 
-map-++ₛ
-  : {A B : Setoid c ℓ}
-    (f : Func A B)
-    (xs ys : List (Setoid.Carrier A))
-  → (open Setoid (Multiset.₀ B))
-  → map (to f) xs ++ map (to f) ys ≈ map (to f) (xs ++ ys)
-map-++ₛ {_} {B} f xs ys =  sym (reflexive (map-++ (to f) xs ys))
-  where
-    open Setoid (Multiset.₀ B)
+  map-++ₛ
+    : {A B : Setoid c ℓ}
+      (f : Func A B)
+      (xs ys : Setoid.Carrier (Multiset.₀ A))
+    → (open Setoid (Multiset.₀ B))
+    → ++ₛ ⟨$⟩ (mapₛ f ⟨$⟩ xs , mapₛ f ⟨$⟩ ys) ≈ mapₛ f ⟨$⟩ (++ₛ ⟨$⟩ (xs , ys))
+  map-++ₛ {A} {B} f xs ys = sym (reflexive (map-++ (to f) xs ys))
+    where
+      open Setoid (Multiset.₀ B)
 
 ++ : NaturalTransformation (-×- ∘F (Multiset ※ Multiset)) Multiset
 ++ = ntHelper record
-    { η = λ X → ++ₛ {X}
+    { η = λ X → ++ₛ
     ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
     }