# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512401677 -32400
# Node ID e3a39aa763689df9d65108cd619c3251cf869d7a
# Parent  ce83d3c28790bf93a8ca387389e94552e278858c
bad case 2

diff -r ce83d3c28790 -r e3a39aa76368 monad→monoidal.agda
--- a/monad→monoidal.agda	Tue Dec 05 00:32:54 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 05 00:34:37 2017 +0900
@@ -38,8 +38,10 @@
      _□_ : {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 [ μ ( x ⊗ y ) o C [ FMap T ( FMap T  ( {!!} □ {!!}  ) ) o  ? ] ]
+     φ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 ) )