blob: c2793cf7312051462a8ea8fbcb05dfbe69ad774b (
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
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Level using (Level; _⊔_)
-- The category of commutative monoids internal to a symmetric monoidal category
module Category.Construction.CMonoids
{o ℓ e : Level}
{𝒞 : Category o ℓ e}
{M : Monoidal 𝒞}
(symmetric : Symmetric M)
where
open import Categories.Functor using (Functor)
open import Categories.Morphism.Reasoning 𝒞
open import Object.Monoid.Commutative symmetric
open Category 𝒞
open Monoidal M
open HomReasoning
open CommutativeMonoid⇒
CMonoids : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ e) e
CMonoids = record
{ Obj = CommutativeMonoid
; _⇒_ = CommutativeMonoid⇒
; _≈_ = λ f g → arr f ≈ arr g
; id = record
{ monoid⇒ = record
{ arr = id
; preserves-μ = identityˡ ○ introʳ ⊗.identity
; preserves-η = identityˡ
}
}
; _∘_ = λ f g → record
{ monoid⇒ = record
{ arr = arr f ∘ arr g
; preserves-μ = glue (preserves-μ f) (preserves-μ g) ○ ∘-resp-≈ʳ (⟺ ⊗.homomorphism)
; preserves-η = glueTrianglesˡ (preserves-η f) (preserves-η g)
}
}
; assoc = assoc
; sym-assoc = sym-assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
; identity² = identity²
; equiv = record
{ refl = refl
; sym = sym
; trans = trans
}
; ∘-resp-≈ = ∘-resp-≈
}
where open Equiv
|
