Mercurial > hg > Members > kono > Proof > category

comparison monoid-monad.agda @ 202:58ee98bbb333

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove an extensionality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Sep 2013 13:26:30 +0900
parents 721cf9d9f5e3
children d6a6dd305da2
comparison
equal deleted inserted replaced
201:eb935f04bf39 202:58ee98bbb333
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
186 186 -- nat-ε TMap = λ a₁ → record { KMap = λ x → x }
187 -- nat-η TMap = λ a₁ → _,_ (ε, M)
188 -- U_T Functor Kleisli A
189 -- U_T FObj = λ B → Σ (Carrier M) (λ x → B) FMap = λ {a₁} {b₁} f₁ x → ( proj₁ x ∙ (proj₁ (KMap f₁ (proj₂ x))) , proj₂ (KMap f₁ (proj₂ x))
190 -- F_T Functor A Kleisli
191 -- F_T FObj = λ a₁ → a₁ FMap = λ {a₁} {b₁} f₁ → record { KMap = λ x → ε M , f₁ x }