blob: 28f214b53d5c1cb4114fcdf88690d88d7cf56b01 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; suc; _⊔_)
module Category.Instance.Monoids (c ℓ : Level) where
import Algebra.Morphism.Bundles as Raw
import Algebra.Morphism.Construct.Composition as Compose
import Algebra.Morphism.Construct.Identity as Identity
open import Algebra using (Monoid)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Relation.Binary using (IsEquivalence)
open Monoid hiding (_≈_)
record MonoidHomomorphism (M N : Monoid c ℓ) : Set (c ⊔ ℓ) where
constructor mk-⇒
field
rawMonoidHomomorphism : Raw.MonoidHomomorphism (rawMonoid M) (rawMonoid N)
open Raw.MonoidHomomorphism rawMonoidHomomorphism public
module _ {M N : Monoid c ℓ} where
-- Pointwise equality of monoid homomorphisms
open MonoidHomomorphism
_≗_ : (f g : MonoidHomomorphism M N) → Set (c ⊔ ℓ)
_≗_ f g = (x : Carrier M) → let open Monoid N in ⟦ f ⟧ x ≈ ⟦ g ⟧ x
infix 4 _≗_
≗-isEquivalence : IsEquivalence _≗_
≗-isEquivalence = record
{ refl = λ x → refl N
; sym = λ f≈g x → sym N (f≈g x)
; trans = λ f≈g g≈h x → trans N (f≈g x) (g≈h x)
}
module ≗ = IsEquivalence ≗-isEquivalence
private
id : {M : Monoid c ℓ} → MonoidHomomorphism M M
id {M} = mk-⇒ record
{ isMonoidHomomorphism = Identity.isMonoidHomomorphism (rawMonoid M) (refl M)
}
compose
: {M N P : Monoid c ℓ}
→ MonoidHomomorphism N P
→ MonoidHomomorphism M N
→ MonoidHomomorphism M P
compose {P = P} f g = mk-⇒ record
{ isMonoidHomomorphism =
Compose.isMonoidHomomorphism
(trans P)
g.isMonoidHomomorphism
f.isMonoidHomomorphism
}
where
module f = MonoidHomomorphism f
module g = MonoidHomomorphism g
open MonoidHomomorphism
-- the category of monoids and monoid homomorphisms
Monoids : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
Monoids = categoryHelper record
{ Obj = Monoid c ℓ
; _⇒_ = MonoidHomomorphism
; _≈_ = _≗_
; id = id
; _∘_ = compose
; assoc = λ {_ _ _ Q} _ → refl Q
; identityˡ = λ {_ B} _ → refl B
; identityʳ = λ {_ B} _ → refl B
; equiv = ≗-isEquivalence
; ∘-resp-≈ = λ {C = C} {f g h i} eq₁ eq₂ x → trans C (⟦⟧-cong f (eq₂ x)) (eq₁ (⟦ i ⟧ x))
}
|
