Mercurial > hg > Members > kono > Proof > category

changeset 741:dfeb296b36d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
assuming C = kleisli
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 05 Dec 2017 00:47:01 +0900
parents e3a39aa76368
children 20f2700a481c
files monad→monoidal.agda
diffstat 1 files changed, 4 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/monad→monoidal.agda	Tue Dec 05 00:34:37 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 05 00:47:01 2017 +0900
@@ -16,8 +16,9 @@
 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 {
+     → ( ε  : (x : Obj C ) → Hom C ( FObj ( Monad.T m ) x ) x )   -- assuming C = kleisli
+     → MonoidalFunctor monoidal monoidal    
+Monad→MonoidalFunctor C M Mono ε  = record {
       MF = Monad.T M
     ; ψ  = NTrans.TMap (Monad.η M )  ( Monoidal.m-i Mono )
     ; isMonodailFunctor = record {
@@ -38,12 +39,8 @@
      _□_ : {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 )
      --                                                        ( T x , T y ) → T ( x , y )
-     hoge : (x : Obj C ) → Hom C ( FObj T x ) x
-     hoge x = {!!}
      φ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 [ FMap T ( hoge x  □ hoge y) o  η ( FObj T x ⊗ FObj T y) ]  
-     --                     μ
-     --      T (( x , y) ) <-  T ( T (x ,y ) ) <- T (  T (x ,y ), T (1 , 1 ) ) <- ( T (x, 1 ) , T (1, y ) )
+     φab (x , y) =  C [ FMap T ( ε x  □ ε y) o  η ( FObj T x ⊗ FObj T y) ]  
 
 import Relation.Binary.PropositionalEquality