3 files changed, 136 insertions, 0 deletions
diff --git a/Functor/Instance/FreeCMonoid.agda b/Functor/Instance/FreeCMonoid.agda
new file mode 100644
index 0000000..1b241b7
--- /dev/null
+++ b/Functor/Instance/FreeCMonoid.agda
@@ -0,0 +1,67 @@
+{-# 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/NaturalTransformation/Instance/EmptyMultiset.agda b/NaturalTransformation/Instance/EmptyMultiset.agda
new file mode 100644
index 0000000..9c3a779
--- /dev/null
+++ b/NaturalTransformation/Instance/EmptyMultiset.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module NaturalTransformation.Instance.EmptyMultiset {c ℓ : Level} where
+
+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 Categories.Functor.Construction.Constant using (const)
+open import Data.List using ([])
+open import Functor.Instance.Multiset {c} {ℓ} using (Multiset)
+open import Relation.Binary using (Setoid)
+
+module Multiset = Functor Multiset
+
+⊤⇒[] : NaturalTransformation (const SingletonSetoid) Multiset
+⊤⇒[] = ntHelper record
+    { η = λ X → Const.function SingletonSetoid (Multiset.₀ X) []
+    ; commute = λ {_} {B} f → Setoid.refl (Multiset.₀ B)
+    }
diff --git a/NaturalTransformation/Instance/MultisetAppend.agda b/NaturalTransformation/Instance/MultisetAppend.agda
new file mode 100644
index 0000000..b0e8bc4
--- /dev/null
+++ b/NaturalTransformation/Instance/MultisetAppend.agda
@@ -0,0 +1,46 @@
+{-# OPTIONS --without-K --safe #-}
+
+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 (_※_)
+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.Functor using (Functor; _∘F_)
+open import Data.List using (List; _++_; map)
+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.Product using (_,_)
+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
+
+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)
+
+++ : NaturalTransformation (-×- ∘F (Multiset ※ Multiset)) Multiset
+++ = ntHelper record
+    { η = λ X → ++ₛ {X}
+    ; commute = λ { {A} {B} f {xs , ys} → map-++ₛ f xs ys }
+    }