|
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
|
|
140
|
5 module monoid-monad {c c₁ c₂ ℓ : Level} { Mono : Monoid c ℓ} where
|
|
130
|
6
|
|
142
|
7 open import Algebra.Structures
|
|
129
|
8 open import HomReasoning
|
|
|
9 open import cat-utility
|
|
|
10 open import Category.Cat
|
|
|
11 open import Category.Sets
|
|
138
|
12 open import Data.Product
|
|
|
13 open import Relation.Binary.Core
|
|
|
14 open import Relation.Binary
|
|
131
|
15
|
|
138
|
16 open Monoid
|
|
|
17
|
|
139
|
18 -- T : A → (M x A)
|
|
134
|
19
|
|
138
|
20 T : Functor (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ })
|
|
|
21 T = record {
|
|
139
|
22 FObj = \a → (Carrier Mono) × a
|
|
|
23 ; FMap = \f → map ( \x → x ) f
|
|
138
|
24 ; isFunctor = record {
|
|
|
25 identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
|
|
|
26 ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )))
|
|
|
27 ; ≈-cong = cong1
|
|
|
28 }
|
|
|
29 } where
|
|
139
|
30 cong1 : {ℓ′ : Level} → {a b : Set ℓ′} { f g : Hom (Sets {ℓ′}) a b} →
|
|
|
31 Sets [ f ≈ g ] → Sets [ map (λ x → x) f ≈ map (λ x → x) g ]
|
|
138
|
32 cong1 _≡_.refl = _≡_.refl
|
|
129
|
33
|
|
139
|
34 Lemma-MM1 : {a b : Obj Sets} {f : Hom Sets a b} →
|
|
|
35 Sets [ Sets [ Functor.FMap T f o (λ x → ε Mono , x) ] ≈
|
|
|
36 Sets [ (λ x → ε Mono , x) o f ] ]
|
|
|
37 Lemma-MM1 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
|
|
|
38 begin
|
|
|
39 Functor.FMap T f o (λ x → ε Mono , x)
|
|
|
40 ≈⟨⟩
|
|
|
41 (λ x → ε Mono , x) o f
|
|
|
42 ∎
|
|
|
43
|
|
|
44 -- a → (ε,a)
|
|
|
45 η : NTrans (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) identityFunctor T
|
|
|
46 η = record {
|
|
|
47 TMap = \a → \(x : a) → ( ε Mono , x ) ;
|
|
|
48 isNTrans = record {
|
|
|
49 commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
|
|
|
50 }
|
|
|
51 }
|
|
|
52
|
|
|
53 -- (m,(m',a)) → (m*m,a)
|
|
|
54
|
|
|
55 open Functor
|
|
|
56
|
|
|
57 muMap : (a : Obj Sets ) → FObj T ( FObj T a ) → Σ (Carrier Mono) (λ x → a )
|
|
|
58 muMap a ( m , ( m' , x ) ) = ( _∙_ Mono m m' , x )
|
|
|
59
|
|
|
60 Lemma-MM2 : {a b : Obj Sets} {f : Hom Sets a b} →
|
|
|
61 Sets [ Sets [ FMap T f o (λ x → muMap a x) ] ≈
|
|
|
62 Sets [ (λ x → muMap b x) o FMap (T ○ T) f ] ]
|
|
|
63 Lemma-MM2 {a} {b} {f} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
|
|
|
64 begin
|
|
|
65 FMap T f o (λ x → muMap a x)
|
|
|
66 ≈⟨⟩
|
|
|
67 (λ x → muMap b x) o FMap (T ○ T) f
|
|
|
68 ∎
|
|
|
69
|
|
|
70 μ : NTrans (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ( T ○ T ) T
|
|
|
71 μ = record {
|
|
|
72 TMap = \a → \x → muMap a x ;
|
|
|
73 isNTrans = record {
|
|
|
74 commute = \{a} {b} {f} → IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))
|
|
|
75 }
|
|
|
76 }
|
|
141
|
77
|
|
|
78 open NTrans
|
|
|
79
|
|
143
|
80 --Lemma-MM32 : ∀{ℓ} {a : Set ℓ } -> {f g : a -> a } -> {x : a } -> ( f ≡ g ) -> ( ( λ x → f x ) ≡ ( λ x → g x ) )
|
|
|
81 --Lemma-MM32 eq = cong ( \f -> \x -> f x ) eq
|
|
|
82
|
|
|
83 --Lemma-MM31 : ( a : Obj ( Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) ) -> {x : FObj T a } → (((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ) ≡ x )
|
|
|
84 --Lemma-MM31 a = {!!}
|
|
142
|
85
|
|
|
86 Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x )
|
|
|
87 Lemma-MM33 = _≡_.refl
|
|
|
88
|
|
143
|
89 Lemma-M-34 : { x : Carrier Mono } -> _≈_ Mono ((_∙_ Mono (ε Mono) x)) x
|
|
|
90 Lemma-M-34 {x} = ( proj₁ ( IsMonoid.identity ( isMonoid Mono )) ) x
|
|
141
|
91
|
|
|
92 MonoidMonad : Monad (Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }) T η μ
|
|
|
93 MonoidMonad = record {
|
|
|
94 isMonad = record {
|
|
|
95 unity1 = \{a} -> Lemma-MM3 {a} ;
|
|
|
96 unity2 = Lemma-MM4 ;
|
|
|
97 assoc = Lemma-MM5
|
|
|
98 }
|
|
|
99 } where
|
|
|
100 A = Sets {c ⊔ c₁ ⊔ c₂ ⊔ ℓ }
|
|
|
101 Lemma-MM3 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
|
102 Lemma-MM3 {a} = let open ≈-Reasoning (Sets) renaming ( _o_ to _*_ ) in
|
|
|
103 begin
|
|
|
104 TMap μ a o TMap η ( FObj T a )
|
|
|
105 ≈⟨⟩
|
|
|
106 ( λ x → ((Mono ∙ ε Mono) (proj₁ x) , proj₂ x ))
|
|
142
|
107 ≈⟨ {!!} ⟩
|
|
141
|
108 ( λ x → x )
|
|
|
109 ≈⟨⟩
|
|
|
110 Id {_} {_} {_} {A} (FObj T a)
|
|
|
111 ∎
|
|
|
112 Lemma-MM4 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
|
|
|
113 Lemma-MM4 = {!!}
|
|
|
114 Lemma-MM5 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ]
|
|
|
115 Lemma-MM5 = {!!}
|
|
|
116
|
|
|
117
|
|
|
118
|
