blob: c51baa9a88d0e1e0824e2b2b5ce849e2eac454e3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
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
}
|
