Mercurial > hg > Members > kono > Proof > category
changeset 738:15ded3383319
add monad to monoidal
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 Dec 2017 17:55:40 +0900 |
| parents | a4792945cd9b |
| children | ce83d3c28790 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 25 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 04 12:36:43 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 04 17:55:40 2017 +0900 @@ -10,10 +10,35 @@ open import Relation.Binary open Functor +open NTrans open import monoidal open import Category.Sets +Monad→MonoidalFunctor : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) ( m : Monad C ) ( monoidal : Monoidal C ) + → MonoidalFunctor monoidal monoidal -- should be monoidal to kleisli-monoidal +Monad→MonoidalFunctor C M Mono = record { + MF = Monad.T M + ; ψ = NTrans.TMap (Monad.η M ) ( Monoidal.m-i Mono ) + ; isMonodailFunctor = record { + φab = record { TMap = φab + ; isNTrans = record { commute = {!!} + } } + ; associativity = {!!} + ; unitarity-idr = {!!} + ; unitarity-idl = {!!} + } + } where + T = Monad.T M + μ = TMap ( Monad.μ M ) + η = TMap ( Monad.η M ) + _⊗_ : (x y : Obj C ) → Obj C + _⊗_ x y = (IsMonoidal._□_ (Monoidal.isMonoidal Mono) ) x y + _□_ : {a b c d : Obj C } ( f : Hom C a c ) ( g : Hom C b d ) → Hom C ( a ⊗ b ) ( c ⊗ d ) + _□_ f g = FMap (Monoidal.m-bi Mono) ( f , g ) + φab : (a : Obj (C × C)) → Hom C (FObj (Functor● C C Mono (Monad.T M)) a) (FObj (Functor⊗ C C Mono (Monad.T M)) a) + φab (x , y ) = C [ μ (x ⊗ y) o {!!} ] + import Relation.Binary.PropositionalEquality Monad→HaskellMonoidalFunctor : {l : Level } (m : Monad (Sets {l} ) ) → HaskellMonoidalFunctor ( Monad.T m )