4 files changed, 152 insertions, 93 deletions
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