|
129
|
1 open import Category -- https://github.com/konn/category-agda
|
|
130
|
2 open import Category.Monoid
|
|
|
3 open import Algebra
|
|
129
|
4 open import Level
|
|
131
|
5 module monoid-monad {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} {A : Category c₁ c₂ ℓ } where
|
|
130
|
6
|
|
129
|
7 open import HomReasoning
|
|
|
8 open import cat-utility
|
|
|
9 open import Category.Cat
|
|
|
10 open import Category.Sets
|
|
|
11
|
|
|
12 -- T : A -> (M x A)
|
|
131
|
13 -- a -> m x a
|
|
|
14 -- m x a -> m' x (m x a)
|
|
129
|
15
|
|
131
|
16 data T1 {c₁ c₂ ℓ : Level} (M : Monoid c₁ ℓ ) ( A : Category c₁ c₂ ℓ ) : Set ( suc ( c₁ ⊔ c₂ ⊔ ℓ) ) where
|
|
|
17 T1a : Obj A -> T1 M A
|
|
|
18 T1t : Obj A -> T1 M A -> T1 M A
|
|
|
19
|
|
|
20 T1HomMap : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {M : Monoid c₁ ℓ } (a : T1 {c₁} {c₂} {ℓ} M A ) (b : T1 {c₁} {c₂} {ℓ} M A) -> Set c₂
|
|
|
21 T1HomMap {c₁} {c₂} {ℓ } { A } (T1a a1 ) (T1a a2 ) = Hom A a1 a2
|
|
|
22 T1HomMap {c₁} {c₂} {ℓ } { A } (T1t a1 t1 ) (T1a a2 ) = Hom A a1 a2
|
|
|
23 T1HomMap {c₁} {c₂} {ℓ } { A } (T1a a1 ) (T1t a2 t2 ) = Hom A a1 a2
|
|
|
24 T1HomMap {c₁} {c₂} {ℓ } { A } (T1t a1 t1 ) (T1t a2 t2 ) = Hom A a1 a2
|
|
|
25
|
|
|
26 record T1Hom1 {c₁ c₂ ℓ : Level} { M : Monoid c₁ ℓ} { A : Category c₁ c₂ ℓ }
|
|
|
27 (a : T1 M A ) (b : T1 M A) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where
|
|
|
28 field
|
|
|
29 T1Map : T1HomMap a b
|
|
|
30
|
|
|
31 open T1Hom1
|
|
|
32 T1Hom = \(a b : T1 M A) -> T1Hom1 {c₁} {c₂} {ℓ} {M} {A} a b
|
|
|
33
|
|
|
34 _*_ : {c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {M : Monoid c₁ ℓ } { a b c : T1 {c₁} {c₂} {ℓ } M A } -> T1Hom1 {c₁} {c₂} {ℓ} b c -> T1Hom1 {c₁} {c₂} {ℓ} a b -> T1Hom1 {c₁} {c₂} {ℓ} a c
|
|
|
35 _*_ {c₁} {c₂} {ℓ } {A} {M} {a} {b} {c} g f = record { T1Map = A [ T1Map g o T1Map f ] }
|
|
129
|
36
|
|
|
37
|
|
131
|
38
|
|
|
39
|
|
|
40
|
|
129
|
41
|
|
131
|
42
|
|
129
|
43
|
|
130
|
44
|
