# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1512461043 -32400
# Node ID e33e9ae1514b2bce6a8556838e4d16ea2914e7cb
# Parent  20f2700a481cd2c7d8d063964cd4c5e702a381b4
.. give up Monad to monoidal functor in general

diff -r 20f2700a481c -r e33e9ae1514b monad→monoidal.agda
--- a/monad→monoidal.agda	Tue Dec 05 01:57:41 2017 +0900
+++ b/monad→monoidal.agda	Tue Dec 05 17:04:03 2017 +0900
@@ -15,68 +15,6 @@
 open import monoidal 
 open import Category.Cat
 
-Monad→MonoidalFunctor : {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) ( m : Monad C ) ( monoidal : Monoidal C )
-     → ( ε  : NTrans C C (Monad.T m ) identityFunctor ) -- assuming C = kleisli
-     → MonoidalFunctor monoidal monoidal    
-Monad→MonoidalFunctor C M Mono ε-nat  = record {
-      MF = Monad.T M
-    ; ψ  = NTrans.TMap (Monad.η M )  ( Monoidal.m-i Mono )
-    ; isMonodailFunctor = record {
-             φab  = record { TMap = φab 
-               ;  isNTrans = record { commute = commute
-               } } 
-         ;   associativity  = {!!}
-         ;   unitarity-idr = {!!}
-         ;   unitarity-idl = {!!}
-      }
-  } where
-     T = Monad.T M
-     μ = TMap ( Monad.μ M )
-     η = TMap ( Monad.η M )
-     -- ε-nat'  : NTrans C C (Monad.T M ) identityFunctor  
-     -- ε-nat'  = record {
-     --    TMap = λ x → {!!}
-     --  ; isNTrans = record { commute = {!!} } }
-     ε = TMap ε-nat
-     _⊗_ : (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 )
-     --                                                        ( T x , T y ) → T ( x , y )
-     φ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 ( ε x  □ ε y) o  η ( FObj T x ⊗ FObj T y) ]  
-     commute :  {a b : Obj (C × C)} {f : Hom (C × C) a b} →
-        C [ C [ FMap (Functor⊗ C C Mono (Monad.T M)) f o φab a ] ≈ C [ φab b o FMap (Functor● C C Mono (Monad.T M)) f ] ]
-     commute {a} {b} {f} =  begin
-                 FMap (Functor⊗ C C Mono (Monad.T M)) f o φab a 
-             ≈⟨⟩
-                 FMap T (proj₁ f □  proj₂ f) o (  FMap T (ε (proj₁ a)  □ ε (proj₂ a)) o (η ( FObj T (proj₁ a) ⊗ FObj T (proj₂ a))))
-             ≈⟨ assoc  ⟩
-                 ( FMap T (proj₁ f □  proj₂ f) o  FMap T (ε (proj₁ a)  □ ε (proj₂ a))) o η ( FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈↑⟨ car (distr T ) ⟩
-                 FMap T ( (proj₁ f □  proj₂ f) o (ε (proj₁ a)  □ ε (proj₂ a))) o η ( FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈↑⟨ car ( fcong T ( distr (Monoidal.m-bi Mono) ))  ⟩
-                 FMap T ( FMap  (Monoidal.m-bi Mono)  ((C × C) [ proj₁ f , proj₂ f o ε (proj₁ a) , ε (proj₂ a) ]) ) o η ( FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈⟨⟩
-                 FMap T ( ( proj₁ f o  ε (proj₁ a) ) □ ( proj₂ f o ε (proj₂ a)  )) o η ( FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈⟨ car ( fcong T ( fcong (Monoidal.m-bi Mono) ( nat ε-nat ,  nat ε-nat ))) ⟩
-                FMap T  ( (ε (proj₁ b) o (FMap T (proj₁ f)) ) □ (  ε (proj₂ b)  o (FMap T (proj₂ f))))  o η (FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈⟨⟩
-                FMap T  (FMap (Monoidal.m-bi Mono) ((C × C) [ ε (proj₁ b) , ε (proj₂ b) o FMap T (proj₁ f) , FMap T (proj₂ f) ]))  o η (FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈⟨   car ( fcong T ( distr (Monoidal.m-bi Mono) ))    ⟩
-                FMap T (C [ ε (proj₁ b) □ ε (proj₂ b) o FMap T (proj₁ f) □ FMap T (proj₂ f) ]) o η (FObj T (proj₁ a) ⊗ FObj T (proj₂ a))
-             ≈⟨ car ( distr T )  ⟩
-                 ( FMap T (ε (proj₁ b) □ ε (proj₂ b)) o  FMap T ((FMap T (proj₁ f) □ FMap T (proj₂ f)))) o η (FObj T (proj₁ a) ⊗  FObj T (proj₂ a))
-             ≈↑⟨ assoc ⟩
-                 FMap T (ε (proj₁ b) □ ε (proj₂ b)) o ( FMap T ((FMap T (proj₁ f) □ FMap T (proj₂ f))) o η (FObj T (proj₁ a) ⊗  FObj T (proj₂ a)))
-             ≈⟨ cdr ( nat ( Monad.η M ))  ⟩
-                 FMap T (ε (proj₁ b) □ ε (proj₂ b)) o ( η (FObj T (proj₁ b) ⊗ FObj T (proj₂ b)) o FMap T (proj₁ f)  □ FMap T (proj₂ f ))
-             ≈⟨ assoc ⟩
-                 ( FMap T (ε (proj₁ b) □ ε (proj₂ b)) o  η (FObj T (proj₁ b) ⊗ FObj T (proj₂ b))) o (FMap T (proj₁ f)  □ FMap T (proj₂ f ))
-             ≈⟨⟩
-                 φab b o FMap (Functor● C C Mono (Monad.T M)) f
-             ∎ 
-             where open ≈-Reasoning C
 
 open import Category.Sets
 import Relation.Binary.PropositionalEquality
@@ -106,6 +44,7 @@
           φ =  HaskellMonoidalFunctor.φ ( Monad→HaskellMonoidalFunctor monad )
           isM = Monoidal.isMonoidal MonoidalSets 
           μ = NTrans.TMap (Monad.μ monad) 
+          η = NTrans.TMap (Monad.η monad) 
           open IsMonoidal
           id : { a : Obj (Sets {l}) } → a → a
           id x = x
@@ -152,7 +91,21 @@
              → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c))
           assocφ = {!!}
           idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
-          idrφ = {!!}
+          idrφ {a} {x} = begin
+                  FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit))
+             ≡⟨⟩
+                  FMap F proj₁ (μ  (a * One) (FMap F (λ f → FMap F (λ g → f , g) (η  One OneObj)) x))
+             ≡⟨ {!!} ⟩
+                 FMap F proj₁ (μ  (a * One) (FMap F (λ f → η ( a * One ) (f , OneObj ) ) x )  ) 
+             ≡⟨ {!!} ⟩
+                 FMap F proj₁ ( FMap F (λ f → {!!}) ( μ {!!} (η {!!} x ) )  )
+             ≡⟨ {!!} ⟩
+                 id1 Sets {!!} x
+             ≡⟨ {!!} ⟩
+                  x
+             ∎ where
+                  open Relation.Binary.PropositionalEquality
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
           idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
           idlφ = {!!}