Add free commutative monoid functor

2 files changed, 36 insertions, 91 deletions

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