-
Notifications
You must be signed in to change notification settings - Fork 60
/
Category.lagda.md
348 lines (291 loc) · 12.9 KB
/
Category.lagda.md
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
<!--
```agda
open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Magma
open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
open import Cat.Functor.Adjoint
open import Cat.Prelude
open import Data.List
import Meta.Idiom
```
-->
```agda
module Algebra.Monoid.Category where
```
<!--
```
open Precategory
open is-semigroup
open is-magma
open Monoid-hom
open Monoid-on
open Functor
open _=>_
open _⊣_
private
map : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → List A → List B
map = Meta.Idiom.map
```
-->
# Category of monoids
<!--
```agda
_ = is-prop
```
-->
The collection of all `Monoid`{.Agda}s relative to some universe level
assembles into a precategory. This is because being a monoid
homomorphism `is a proposition`{.Agda ident=is-prop}, and so does not
raise the [h-level] of the Hom-sets.
[h-level]: 1Lab.HLevel.html
```agda
instance
H-Level-Monoid-hom
: ∀ {ℓ ℓ'} {s : Type ℓ} {t : Type ℓ'}
→ ∀ {x : Monoid-on s} {y : Monoid-on t} {f} {n}
→ H-Level (Monoid-hom x y f) (suc n)
H-Level-Monoid-hom {y = M} = prop-instance λ x y i →
record { pres-id = M .has-is-set _ _ (x .pres-id) (y .pres-id) i
; pres-⋆ = λ a b → M .has-is-set _ _ (x .pres-⋆ a b) (y .pres-⋆ a b) i
}
```
It's routine to check that the identity is a monoid homomorphism and
that composites of homomorphisms are again homomorphisms; This means
that `Monoid-on`{.Agda} assembles into a structure thinly displayed over
the category of sets, so that we may appeal to general results about
[[displayed categories]] to reason about the category of monoids.
```agda
Monoid-structure : ∀ ℓ → Thin-structure ℓ Monoid-on
Monoid-structure ℓ .is-hom f A B = el! $ Monoid-hom A B f
Monoid-structure ℓ .id-is-hom .pres-id = refl
Monoid-structure ℓ .id-is-hom .pres-⋆ x y = refl
Monoid-structure ℓ .∘-is-hom f g p1 p2 .pres-id =
ap f (p2 .pres-id) ∙ p1 .pres-id
Monoid-structure ℓ .∘-is-hom f g p1 p2 .pres-⋆ x y =
ap f (p2 .pres-⋆ _ _) ∙ p1 .pres-⋆ _ _
Monoid-structure ℓ .id-hom-unique mh _ i .identity = mh .pres-id i
Monoid-structure ℓ .id-hom-unique mh _ i ._⋆_ x y = mh .pres-⋆ x y i
Monoid-structure ℓ .id-hom-unique {s = s} {t = t} mh _ i .has-is-monoid =
is-prop→pathp
(λ i → hlevel {T = is-monoid (mh .pres-id i) (λ x y → mh .pres-⋆ x y i)} 1)
(s .has-is-monoid)
(t .has-is-monoid)
i
Monoids : ∀ ℓ → Precategory (lsuc ℓ) ℓ
Monoids ℓ = Structured-objects (Monoid-structure ℓ)
Monoids-is-category : ∀ {ℓ} → is-category (Monoids ℓ)
Monoids-is-category = Structured-objects-is-category (Monoid-structure _)
```
By standard nonsense, then, the category of monoids admits a [[faithful
functor]] into the category of sets.
```agda
Mon↪Sets : ∀ {ℓ} → Functor (Monoids ℓ) (Sets ℓ)
Mon↪Sets = Forget-structure (Monoid-structure _)
```
## Free objects {defines=free-monoid}
We piece together some properties of `lists`{.Agda ident=List} to show
that, if $A$ is a set, then $\rm{List}(A)$ is an object of
`Monoids`{.Agda}; The operation is list concatenation, and the identity
element is the empty list.
```agda
List-is-monoid : ∀ {ℓ} {A : Type ℓ} → is-set A
→ Monoid-on (List A)
List-is-monoid aset .identity = []
List-is-monoid aset ._⋆_ = _++_
List-is-monoid aset .has-is-monoid .idl = refl
List-is-monoid aset .has-is-monoid .idr = ++-idr _
List-is-monoid aset .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set =
ListPath.is-set→List-is-set aset
List-is-monoid aset .has-is-monoid .has-is-semigroup .associative {x} {y} {z} =
sym (++-assoc x y z)
```
We prove that the assignment $X \mapsto \rm{List}(X)$ is functorial;
We call this functor `Free`{.Agda}, since it is a [[left adjoint]] to the
`Forget`{.Agda} functor defined above: it solves the problem of turning
a `set`{.Agda ident=Set} into a monoid in the most efficient way.
```agda
Free-monoid : ∀ {ℓ} → Functor (Sets ℓ) (Monoids ℓ)
Free-monoid .F₀ A = el! (List ∣ A ∣) , List-is-monoid (A .is-tr)
```
The action on morphisms is given by `map`{.Agda}, which preserves the
monoid identity definitionally; We must prove that it preserves
concatenation, identity and composition by induction on the list.
```agda
Free-monoid .F₁ f = total-hom (map f) record { pres-id = refl ; pres-⋆ = map-++ f }
Free-monoid .F-id = ext map-id
Free-monoid .F-∘ f g = ext map-∘ where
map-∘ : ∀ xs → map (λ x → f (g x)) xs ≡ map f (map g xs)
map-∘ [] = refl
map-∘ (x ∷ xs) = ap (f (g x) ∷_) (map-∘ xs)
```
We refer to the adjunction counit as `fold`{.Agda}, since it has the
effect of multiplying all the elements in the list together. It "folds"
it up into a single value.
```agda
fold : ∀ {ℓ} (X : Monoid ℓ) → List (X .fst) → X .fst
fold (M , m) = go where
module M = Monoid-on m
go : List M → M
go [] = M.identity
go (x ∷ xs) = x M.⋆ go xs
```
We prove that `fold` is a monoid homomorphism, and that it is a natural
transformation, hence worthy of being an adjunction counit.
```agda
fold-++ : ∀ {ℓ} {X : Monoid ℓ} (xs ys : List (X .fst))
→ fold X (xs ++ ys) ≡ Monoid-on._⋆_ (X .snd) (fold X xs) (fold X ys)
fold-++ {X = X} = go where
module M = Monoid-on (X .snd)
go : ∀ xs ys → _
go [] ys = sym M.idl
go (x ∷ xs) ys =
fold X (x ∷ xs ++ ys) ≡⟨⟩
x M.⋆ fold X (xs ++ ys) ≡⟨ ap (_ M.⋆_) (go xs ys) ⟩
x M.⋆ (fold X xs M.⋆ fold X ys) ≡⟨ M.associative ⟩
fold X (x ∷ xs) M.⋆ fold X ys ∎
fold-natural : ∀ {ℓ} {X Y : Monoid ℓ} f → Monoid-hom (X .snd) (Y .snd) f
→ ∀ xs → fold Y (map f xs) ≡ f (fold X xs)
fold-natural f mh [] = sym (mh .pres-id)
fold-natural {X = X} {Y} f mh (x ∷ xs) =
f x Y.⋆ fold Y (map f xs) ≡⟨ ap (_ Y.⋆_) (fold-natural f mh xs) ⟩
f x Y.⋆ f (fold X xs) ≡⟨ sym (mh .pres-⋆ _ _) ⟩
f (x X.⋆ fold X xs) ∎
where
module X = Monoid-on (X .snd)
module Y = Monoid-on (Y .snd)
```
Proving that it satisfies the `zig`{.Agda} triangle identity is the
lemma `fold-pure`{.Agda} below.
```agda
fold-pure : ∀ {ℓ} {X : Set ℓ} (xs : List ∣ X ∣)
→ fold (List ∣ X ∣ , List-is-monoid (X .is-tr)) (map (λ x → x ∷ []) xs)
≡ xs
fold-pure [] = refl
fold-pure {X = X} (x ∷ xs) = ap (x ∷_) (fold-pure {X = X} xs)
Free-monoid⊣Forget : ∀ {ℓ} → Free-monoid {ℓ} ⊣ Mon↪Sets
Free-monoid⊣Forget .unit .η _ x = x ∷ []
Free-monoid⊣Forget .unit .is-natural x y f = refl
Free-monoid⊣Forget .counit .η M = total-hom (fold _) record { pres-id = refl ; pres-⋆ = fold-++ }
Free-monoid⊣Forget .counit .is-natural x y th =
ext $ fold-natural (th .hom) (th .preserves)
Free-monoid⊣Forget .zig {A = A} =
ext $ fold-pure {X = A}
Free-monoid⊣Forget .zag {B = B} i x = B .snd .idr {x = x} i
```
This concludes the proof that `Monoids`{.Agda} has free objects. We now
prove that monoids are equivalently algebras for the `List`{.Agda}
monad, i.e. that the `Free-monoid⊣Forget`{.Agda} adjunction is [monadic]. More
specifically, we show that the canonically-defined `comparison`{.Agda
ident=Comparison} functor is [[fully faithful]] (list algebra homomoprhisms
are equivalent to monoid homomorphisms) and that it is [[split
essentially surjective]].
[monadic]: Cat.Functor.Adjoint.Monadic.html
```agda
Monoid-is-monadic : ∀ {ℓ} → is-monadic (Free-monoid⊣Forget {ℓ})
Monoid-is-monadic {ℓ} = ff+split-eso→is-equivalence it's-ff it's-eso where
open import Cat.Diagram.Monad
comparison = Comparison (Free-monoid⊣Forget {ℓ})
module comparison = Functor comparison
it's-ff : is-fully-faithful comparison
it's-ff {x} {y} = is-iso→is-equiv (iso from from∘to to∘from) where
module x = Monoid-on (x .snd)
module y = Monoid-on (y .snd)
```
First, for full-faithfulness, it suffices to prove that the morphism
part of `comparison`{.Agda} is an `isomorphism`{.Agda ident=iso}. Hence,
define an inverse; It suffices to show that the underlying map of the
algebra homomorphism is a monoid homomorphism, which follows from the
properties of monoids:
```agda
from : Algebra-hom _ _ (comparison.₀ x) (comparison.₀ y) → Monoids ℓ .Hom x y
from alg .hom = alg .Algebra-hom.morphism
from alg .preserves .pres-id = happly (alg .Algebra-hom.commutes) []
from alg .preserves .pres-⋆ a b =
f (a x.⋆ b) ≡˘⟨ ap f (ap (a x.⋆_) x.idr) ⟩
f (a x.⋆ (b x.⋆ x.identity)) ≡⟨ (λ i → alg .Algebra-hom.commutes i (a ∷ b ∷ [])) ⟩
f a y.⋆ (f b y.⋆ y.identity) ≡⟨ ap (f a y.⋆_) y.idr ⟩
f a y.⋆ f b ∎
where f = alg .Algebra-hom.morphism
```
The proofs that this is a quasi-inverse is immediate, since both "being
an algebra homomorphism" and "being a monoid homomorphism" are
properties of the underlying map.
```agda
from∘to : is-right-inverse from comparison.₁
from∘to x = trivial!
to∘from : is-left-inverse from comparison.₁
to∘from x = trivial!
```
Showing that the functor is essentially surjective is significantly more
complicated. We must show that we can recover a monoid from a List
algebra (a "fold"): We take the unit element to be the fold of the empty
list, and the binary operation $x \star y$ to be the fold of the list
$[x,y]$.
```agda
it's-eso : is-split-eso comparison
it's-eso (A , alg) = monoid , the-iso where
open Algebra-on
open Algebra-hom
import Cat.Reasoning (Eilenberg-Moore _ (L∘R (Free-monoid⊣Forget {ℓ}))) as R
monoid : Monoids ℓ .Ob
monoid .fst = A
monoid .snd .identity = alg .ν []
monoid .snd ._⋆_ a b = alg .ν (a ∷ b ∷ [])
```
It suffices, through _incredibly_ tedious calculations, to show that
these data assembles into a monoid:
```agda
monoid .snd .has-is-monoid = has-is-m where abstract
has-is-m : is-monoid (alg .ν []) (monoid .snd ._⋆_)
has-is-m .has-is-semigroup = record
{ has-is-magma = record { has-is-set = A .is-tr }
; associative = λ {x} {y} {z} →
alg .ν (⌜ x ⌝ ∷ alg .ν (y ∷ z ∷ []) ∷ []) ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
alg .ν (alg .ν (x ∷ []) ∷ alg .ν (y ∷ z ∷ []) ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
alg .ν (x ∷ y ∷ z ∷ []) ≡˘⟨ happly (alg .ν-mult) _ ⟩
alg .ν (alg .ν (x ∷ y ∷ []) ∷ ⌜ alg .ν (z ∷ []) ⌝ ∷ []) ≡⟨ ap! (happly (alg .ν-unit) z) ⟩
alg .ν (alg .ν (x ∷ y ∷ []) ∷ z ∷ []) ∎
}
has-is-m .idl {x} =
alg .ν (alg .ν [] ∷ ⌜ x ⌝ ∷ []) ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
alg .ν (alg .ν [] ∷ alg .ν (x ∷ []) ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
alg .ν (x ∷ []) ≡⟨ happly (alg .ν-unit) x ⟩
x ∎
has-is-m .idr {x} =
alg .ν (⌜ x ⌝ ∷ alg .ν [] ∷ []) ≡˘⟨ ap¡ (happly (alg .ν-unit) x) ⟩
alg .ν (alg .ν (x ∷ []) ∷ alg .ν [] ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
alg .ν (x ∷ []) ≡⟨ happly (alg .ν-unit) x ⟩
x ∎
```
The most important lemma is that `folding`{.Agda ident=fold} a list
using this monoid recovers the original algebra multiplication, which we
can show by induction on the list:
```agda
recover : ∀ x → fold _ x ≡ alg .ν x
recover [] = refl
recover (x ∷ xs) =
alg .ν (x ∷ fold _ xs ∷ []) ≡⟨ ap₂ (λ e f → alg .ν (e ∷ f ∷ [])) (sym (happly (alg .ν-unit) x)) (recover xs) ⟩
alg .ν (alg .ν (x ∷ []) ∷ alg .ν xs ∷ []) ≡⟨ happly (alg .ν-mult) _ ⟩
alg .ν (x ∷ xs ++ []) ≡⟨ ap (alg .ν) (++-idr _) ⟩
alg .ν (x ∷ xs) ∎
```
We must then show that the image of this monoid under
`Comparison`{.Agda} is isomorphic to the original algebra. Fortunately,
this follows from the `recover`{.Agda} lemma above; The isomorphism
itself is given by the identity function in both directions, since the
recovered monoid has the same underlying type as the List-algebra!
```agda
into : Algebra-hom _ _ (comparison.₀ monoid) (A , alg)
into .morphism = λ x → x
into .commutes = funext (λ x → recover x ∙ ap (alg .ν) (sym (map-id x)))
from : Algebra-hom _ _ (A , alg) (comparison.₀ monoid)
from .morphism = λ x → x
from .commutes =
funext (λ x → sym (recover x) ∙ ap (fold _) (sym (map-id x)))
the-iso : comparison.₀ monoid R.≅ (A , alg)
the-iso = R.make-iso into from (Algebra-hom-path _ refl) (Algebra-hom-path _ refl)
```