Add free/forget multiset adjunction

4 files changed, 218 insertions, 6 deletions

diff --git a/Adjoint/Instance/List.agda b/Adjoint/Instance/List.agda
index f3bf061..1b65985 100644
--- a/Adjoint/Instance/List.agda
+++ b/Adjoint/Instance/List.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Level using (Level; _⊔_; suc; 0ℓ)
+open import Level using (Level; _⊔_; suc)
 
 module Adjoint.Instance.List {ℓ : Level} where
 
diff --git a/Adjoint/Instance/Multiset.agda b/Adjoint/Instance/Multiset.agda
new file mode 100644
index 0000000..c51baa9
--- /dev/null
+++ b/Adjoint/Instance/Multiset.agda
@@ -0,0 +1,112 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level; _⊔_; suc; 0ℓ)
+
+module Adjoint.Instance.Multiset {ℓ : Level} where
+
+open import Category.Instance.Setoids.SymmetricMonoidal {ℓ} {ℓ} using (Setoids-×)
+
+private
+  module S = Setoids-×
+
+import Categories.Object.Monoid S.monoidal as MonoidObject
+import Data.List as L
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
+import Functor.Forgetful.Instance.CMonoid S.symmetric as CMonoid
+import Functor.Forgetful.Instance.Monoid S.monoidal as Monoid
+import Object.Monoid.Commutative S.symmetric as CMonoidObject
+
+open import Categories.Adjoint using (_⊣_)
+open import Categories.Category using (Category)
+open import Categories.Functor using (Functor; id; _∘F_)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Category.Construction.CMonoids using (CMonoids)
+open import Data.CMonoid using (toCMonoid; toCMonoid⇒)
+open import Data.Monoid using (toMonoid; toMonoid⇒)
+open import Data.Opaque.Multiset using ([-]ₛ; Multisetₛ; foldₛ; ++ₛ-homo; []ₛ-homo; fold-mapₛ; fold)
+open import Data.Product using (_,_; uncurry)
+open import Data.Setoid using (∣_∣)
+open import Function using (_⟶ₛ_; _⟨$⟩_)
+open import Functor.Free.Instance.CMonoid {ℓ} {ℓ} using (Multisetₘ; mapₘ; MultisetCMonoid) renaming (Free to Free′)
+open import Relation.Binary using (Setoid)
+
+open CMonoidObject using (CommutativeMonoid; CommutativeMonoid⇒)
+open CommutativeMonoid using (Carrier; monoid; identityʳ)
+open CommutativeMonoid⇒ using (arr; monoid⇒)
+open MonoidObject using (Monoid; Monoid⇒)
+open Monoid⇒ using (preserves-μ; preserves-η)
+
+CMon[S] : Category (suc ℓ) ℓ ℓ
+CMon[S] = CMonoids S.symmetric
+
+Free : Functor S.U CMon[S]
+Free = Free′
+
+Forget : Functor CMon[S] S.U
+Forget = Monoid.Forget ∘F CMonoid.Forget
+
+opaque
+  unfolding [-]ₛ
+  map-[-]ₛ
+      : {X Y : Setoid ℓ ℓ}
+        (f : X ⟶ₛ Y)
+        {x : ∣ X ∣}
+      → (open Setoid (Multisetₛ Y))
+      → [-]ₛ ⟨$⟩ (f ⟨$⟩ x)
+      ≈ arr (mapₘ f) ⟨$⟩ ([-]ₛ ⟨$⟩ x)
+  map-[-]ₛ {X} {Y} f {x} = Setoid.refl (Multisetₛ Y)
+
+unit : NaturalTransformation id (Forget ∘F Free)
+unit = ntHelper record
+    { η = λ X → [-]ₛ {ℓ} {ℓ} {X}
+    ; commute = map-[-]ₛ
+    }
+
+opaque
+  unfolding toMonoid MultisetCMonoid
+  foldₘ : (X : CommutativeMonoid) → CommutativeMonoid⇒ (Multisetₘ (Carrier X)) X
+  foldₘ X .monoid⇒ .Monoid⇒.arr = foldₛ (toCMonoid X)
+  foldₘ X .monoid⇒ .preserves-μ {xs , ys} = ++ₛ-homo (toCMonoid X) xs ys
+  foldₘ X .monoid⇒ .preserves-η {_} = []ₛ-homo (toCMonoid X)
+
+opaque
+  unfolding foldₘ toMonoid⇒
+  fold-mapₘ
+      : {X Y : CommutativeMonoid}
+        (f : CommutativeMonoid⇒ X Y)
+        {x : ∣ Multisetₛ (Carrier X) ∣}
+      → (open Setoid (Carrier Y))
+      → arr (foldₘ Y) ⟨$⟩ (arr (mapₘ (arr f)) ⟨$⟩ x)
+      ≈ arr f ⟨$⟩ (arr (foldₘ X) ⟨$⟩ x)
+  fold-mapₘ {X} {Y} f = uncurry (fold-mapₛ (toCMonoid X) (toCMonoid Y)) (toCMonoid⇒ X Y f)
+
+counit : NaturalTransformation (Free ∘F Forget) id
+counit = ntHelper record
+    { η = foldₘ
+    ; commute = fold-mapₘ
+    }
+
+opaque
+  unfolding foldₘ fold Multisetₛ
+  zig : (Aₛ  : Setoid ℓ ℓ)
+        {xs : ∣ Multisetₛ Aₛ ∣}
+      → (open Setoid (Multisetₛ Aₛ))
+      → arr (foldₘ (Multisetₘ Aₛ)) ⟨$⟩ (arr (mapₘ [-]ₛ) ⟨$⟩ xs) ≈ xs
+  zig Aₛ {L.[]} = ↭.↭-refl Aₛ
+  zig Aₛ {x L.∷ xs} = ↭.prep (Setoid.refl Aₛ) (zig Aₛ)
+
+opaque
+  unfolding foldₘ fold
+  zag : (M : CommutativeMonoid)
+        {x : ∣ Carrier M ∣}
+      → (open Setoid (Carrier M))
+      → arr (foldₘ M) ⟨$⟩ ([-]ₛ ⟨$⟩ x) ≈ x
+  zag M {x} = Setoid.sym (Carrier M) (identityʳ M {x , _})
+
+Multiset⊣ : Free ⊣ Forget
+Multiset⊣ = record
+    { unit = unit
+    ; counit = counit
+    ; zig = λ {X} → zig X
+    ; zag = λ {M} → zag M
+    }
diff --git a/Data/Opaque/Multiset.agda b/Data/Opaque/Multiset.agda
index 2ba0a0e..99501d6 100644
--- a/Data/Opaque/Multiset.agda
+++ b/Data/Opaque/Multiset.agda
@@ -4,14 +4,20 @@
 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 Data.List.Relation.Binary.Permutation.Setoid as ↭ using (↭-setoid; prep)
+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 Data.Product using (_,_)
-open import Data.Product using (uncurry′)
+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 Function using (_⟶ₛ_; Func; _⟨$⟩_)
+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)
@@ -50,7 +56,11 @@ opaque
 
   ∷ₛ : Aₛ ×ₛ Multisetₛ Aₛ ⟶ₛ Multisetₛ Aₛ
   ∷ₛ .to = uncurry′ _∷_
-  ∷ₛ .cong = uncurry′ prep
+  ∷ₛ .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)
@@ -65,3 +75,57 @@ opaque
       → (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
diff --git a/Functor/Forgetful/Instance/CMonoid.agda b/Functor/Forgetful/Instance/CMonoid.agda
new file mode 100644
index 0000000..fd8ecc1
--- /dev/null
+++ b/Functor/Forgetful/Instance/CMonoid.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Symmetric using (Symmetric)
+open import Level using (Level)
+
+module Functor.Forgetful.Instance.CMonoid
+    {o ℓ e : Level}
+    {S : Category o ℓ e}
+    {monoidal : Monoidal S}
+    (symmetric : Symmetric monoidal)
+  where
+
+open import Categories.Category.Construction.Monoids monoidal using (Monoids)
+open import Categories.Functor using (Functor)
+open import Category.Construction.CMonoids symmetric using (CMonoids)
+open import Function using (id)
+open import Object.Monoid.Commutative using (CommutativeMonoid; CommutativeMonoid⇒)
+
+private
+  module S = Category S
+
+open CommutativeMonoid
+open CommutativeMonoid⇒
+open Functor
+open S.Equiv using (refl)
+
+Forget : Functor CMonoids Monoids
+Forget .F₀ = monoid
+Forget .F₁ = monoid⇒
+Forget .identity = refl
+Forget .homomorphism = refl
+Forget .F-resp-≈ = id
+
+module Forget = Functor Forget