blob: 79bb03240755d4da6d7581d663d5b3a94f9118f5 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; suc; _⊔_)
module Category.Instance.CMonoids (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 (CommutativeMonoid)
open import Categories.Category using (Category)
open import Categories.Category.Helper using (categoryHelper)
open import Relation.Binary using (IsEquivalence)
open import Function using (Func; _⟶ₛ_)
open CommutativeMonoid hiding (_≈_)
open Func
record CMonoidHomomorphism (M N : CommutativeMonoid c ℓ) : Set (c ⊔ ℓ) where
constructor mk-⇒
field
rawMonoidHomomorphism : Raw.MonoidHomomorphism (rawMonoid M) (rawMonoid N)
open Raw.MonoidHomomorphism rawMonoidHomomorphism public
func : setoid M ⟶ₛ setoid N
func .to = ⟦_⟧
func .cong = ⟦⟧-cong
module _ {M N : CommutativeMonoid c ℓ} where
-- Pointwise equality of monoid homomorphisms
open CMonoidHomomorphism
_≗_ : (f g : CMonoidHomomorphism M N) → Set (c ⊔ ℓ)
_≗_ f g = (x : Carrier M) → let open CommutativeMonoid 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 : CommutativeMonoid c ℓ} → CMonoidHomomorphism M M
id {M} = mk-⇒ record
{ isMonoidHomomorphism = Identity.isMonoidHomomorphism (rawMonoid M) (refl M)
}
compose
: {M N P : CommutativeMonoid c ℓ}
→ CMonoidHomomorphism N P
→ CMonoidHomomorphism M N
→ CMonoidHomomorphism M P
compose {P = P} f g = mk-⇒ record
{ isMonoidHomomorphism =
Compose.isMonoidHomomorphism
(trans P)
g.isMonoidHomomorphism
f.isMonoidHomomorphism
}
where
module f = CMonoidHomomorphism f
module g = CMonoidHomomorphism g
open CMonoidHomomorphism
-- the category of commutative monoids and monoid homomorphisms
CMonoids : Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
CMonoids = categoryHelper record
{ Obj = CommutativeMonoid c ℓ
; _⇒_ = CMonoidHomomorphism
; _≈_ = _≗_
; 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))
}
|
