|
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
|
|
130
|
5 module monoid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ } where
|
|
|
6
|
|
|
7 open import Category.HomReasoning
|
|
129
|
8 open import HomReasoning
|
|
|
9 open import cat-utility
|
|
|
10 open import Category.Cat
|
|
|
11 open import Category.Sets
|
|
|
12 open import Data.Product
|
|
|
13 open import Relation.Binary.Core
|
|
|
14 open import Relation.Binary
|
|
|
15
|
|
|
16
|
|
|
17 MC : Category (suc zero) c (suc (ℓ ⊔ c))
|
|
|
18 MC = MONOID Mono
|
|
|
19
|
|
|
20 -- T : A -> (M x A)
|
|
|
21
|
|
|
22 T : ∀{ℓ′} -> Functor (Sets {ℓ′}) (Sets {ℓ ⊔ ℓ′} )
|
|
|
23 T = record {
|
|
|
24 FObj = \a -> MS × a
|
|
|
25 ; FMap = \f -> map ( \x -> x ) f
|
|
|
26 ; isFunctor = record {
|
|
|
27 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
|
|
|
28 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
|
|
|
29 ; ≈-cong = cong1
|
|
|
30 }
|
|
|
31 } where
|
|
|
32 cong1 : {ℓ′ : Level} -> {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} -> Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
|
|
|
33 cong1 refl = refl
|
|
|
34
|
|
|
35
|
|
130
|
36 -- Forgetful Functor
|
|
129
|
37
|
|
130
|
38 open Functor
|
|
|
39 F : Functor MC Sets
|
|
|
40 F = record {
|
|
|
41 FObj = \a -> { s : Obj Sets } -> s
|
|
|
42 ; FMap = \f -> ? -- {a : Obj Sets} { g : Hom Sets (FObj F *) (FObj F ((Mor MC f) *)) } -> g
|
|
|
43 ; isFunctor = record {
|
|
|
44 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
|
|
|
45 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
|
|
|
46 -- ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
|
|
|
47 }
|
|
|
48 }
|
|
129
|
49
|
|
130
|
50 -- Gerator
|
|
|
51
|
|
|
52 G : Functor Sets MC
|
|
|
53 G = record {
|
|
|
54 FObj = \a -> *
|
|
|
55 ; FMap = \f -> { g : Hom MC * * } -> Mor MC
|
|
|
56 ; isFunctor = record {
|
|
|
57 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC ))
|
|
|
58 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC )))
|
|
|
59 ; ≈-cong = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory MC )))
|
|
|
60 }
|
|
|
61 }
|
