|
129
|
1 open import Category -- https://github.com/konn/category-agda
|
|
|
2 open import Level
|
|
|
3 --open import Category.HomReasoning
|
|
|
4 open import HomReasoning
|
|
|
5 open import cat-utility
|
|
|
6 open import Category.Cat
|
|
|
7 open import Category.Sets
|
|
|
8 open import Algebra
|
|
|
9 open import Category.Monoid
|
|
|
10 open import Data.Product
|
|
|
11 open import Relation.Binary.Core
|
|
|
12 open import Relation.Binary
|
|
|
13
|
|
|
14 module monooid-monad {c c₁ c₂ ℓ : Level} { MS : Set ℓ } { Mono : Monoid c ℓ} {A : Category c₁ c₂ ℓ } where
|
|
|
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
|
|
|
36
|
|
|
37
|
