Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 300:d6a6dd305da2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
arrow and lambda fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 29 Sep 2013 14:01:07 +0900
parents 58ee98bbb333
children 93cf0a6c21fe
comparison
equal deleted inserted replaced
299:8c72f5284bc8 300:d6a6dd305da2
109 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c 109 postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c c
110 110
111 -- Multi Arguments Functional Extensionality 111 -- Multi Arguments Functional Extensionality
112 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } → 112 extensionality30 : {f g : Carrier M → Carrier M → Carrier M → Carrier M } →
113 (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g ) 113 (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g )
114 extensionality30 eq = extensionality ( \x -> extensionality ( \y -> extensionality (eq x y) ) ) 114 extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) )
115 115
116 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x ) 116 Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x )
117 Lemma-MM9 = extensionality Lemma-MM34 117 Lemma-MM9 = extensionality Lemma-MM34
118 118
119 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) 119 Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x )
169 ≈⟨⟩ 169 ≈⟨⟩
170 TMap μ a o FMap T (TMap μ a) 170 TMap μ a o FMap T (TMap μ a)
171 ∎ 171 ∎
172 172
173 173
174 F : (m : Carrier M) -> { a b : Obj A } -> ( f : a -> b ) -> Hom A a ( FObj T b ) 174 F : (m : Carrier M) → { a b : Obj A } → ( f : a → b ) → Hom A a ( FObj T b )
175 F m {a} {b} f = \(x : a ) -> ( m , ( f x) ) 175 F m {a} {b} f = λ (x : a ) → ( m , ( f x) )
176 176
177 postulate m m' : Carrier M 177 postulate m m' : Carrier M
178 postulate a b c' : Obj A 178 postulate a b c' : Obj A
179 postulate f : b -> c' 179 postulate f : b → c'
180 postulate g : a -> b 180 postulate g : a → b
181 181
182 Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g) 182 Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g)
183 183
184 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad} 184 open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad}
185 185