blob: 7a64d88468f4ec5eac1cf92760423cabcb0174eb (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level; suc; _⊔_)
module Category.Cartesian.Instance.CMonoids {c ℓ : Level} where
import Algebra.Construct.DirectProduct as ×
import Algebra.Construct.Terminal as Term
import Algebra.Morphism.Construct.DirectProduct as ×-⇒
import Algebra.Morphism.Construct.Terminal as Term-⇒
open import Algebra using (CommutativeMonoid)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Object.Terminal using (Terminal)
open import Category.Instance.CMonoids c ℓ using (CMonoids; CMonoidHomomorphism; mk-⇒)
open import Data.Product using (_,_)
open import Data.Unit.Polymorphic using (tt)
open CMonoidHomomorphism using (isMonoidHomomorphism)
open CommutativeMonoid using (rawMonoid; refl; sym)
terminal : Terminal CMonoids
terminal = record
{ ⊤ = Term.commutativeMonoid
; ⊤-is-terminal = record
{ ! = λ {M} → mk-⇒ record { isMonoidHomomorphism = Term-⇒.isMonoidHomomorphism (rawMonoid M) }
; !-unique = λ _ _ → tt
}
}
products : BinaryProducts CMonoids
products = record
{ product = λ {M N} → record
{ A×B = ×.commutativeMonoid M N
; π₁ = mk-⇒ record { isMonoidHomomorphism = ×-⇒.Monoid-Export.proj₁ {refl = refl M} }
; π₂ = mk-⇒ record { isMonoidHomomorphism = ×-⇒.Monoid-Export.proj₂ {refl = refl N} }
; ⟨_,_⟩ = λ {C} f g → mk-⇒ record
{ isMonoidHomomorphism = ×-⇒.Monoid-Export.< isMonoidHomomorphism f , isMonoidHomomorphism g > }
; project₁ = λ _ → refl M
; project₂ = λ _ → refl N
; unique = λ eq₁ eq₂ x → sym M (eq₁ x) , sym N (eq₂ x)
}
}
CMonoids-Cartesian : Cartesian CMonoids
CMonoids-Cartesian = record
{ terminal = terminal
; products = products
}
CMonoids-CC : CartesianCategory (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
CMonoids-CC = record { cartesian = CMonoids-Cartesian }
module CMonoids-CC = CartesianCategory CMonoids-CC
|
