# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511509114 -32400
# Node ID a017ed40dd77901038fbecc1563d7bc0fe29d914
# Parent  f2e617dc2c212507ac54fa58836c93b269e65aed
Applicative law → Monoidal law begin

diff -r f2e617dc2c21 -r a017ed40dd77 monoidal.agda
--- a/monoidal.agda	Fri Nov 24 14:27:07 2017 +0900
+++ b/monoidal.agda	Fri Nov 24 16:38:34 2017 +0900
@@ -519,6 +519,98 @@
      <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        --  ** mono  x y 
      <*> {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ mono ( x , y ))
 
+Applicative→Monoidal :  {c : Level} ( F : Functor (Sets {c}) (Sets {c}) ) → (mf : Applicative F )
+   → IsApplicative F ( Applicative.pure mf ) ( Applicative.<*> mf ) 
+   → MonoidalFunctor {_} {c} {_} {Sets} {Sets} MonoidalSets MonoidalSets
+Applicative→Monoidal F mf ismf = record {
+      MF = F
+    ; ψ  = λ x → unit
+    ; isMonodailFunctor = record {
+             φab  = record { TMap = λ x → φ ; isNTrans = record { commute = comm0 } }
+         ;   associativity  = λ {a b c} → comm1 {a} {b} {c}
+         ;   unitarity-idr = λ {a b} → comm2 {a} {b}
+         ;   unitarity-idl = λ {a b} → comm3 {a} {b}
+      }
+  } where
+      open Monoidal 
+      open IsMonoidal hiding ( _■_ ;  _□_ )
+      M = MonoidalSets
+      isM = Monoidal.isMonoidal MonoidalSets 
+      unit = Applicative.pure mf OneObj
+      _⊗_ : (x y : Obj Sets ) → Obj Sets
+      _⊗_ x y =  (IsMonoidal._□_ (Monoidal.isMonoidal M) ) x y
+      _□_ : {a b c d : Obj Sets } ( f : Hom Sets a c ) ( g : Hom Sets b d ) → Hom Sets ( a ⊗ b ) ( c ⊗ d )
+      _□_ f g = FMap (m-bi M) ( f , g )
+      φ : {x : Obj (Sets × Sets) } → Hom Sets (FObj (Functor● Sets Sets MonoidalSets F) x) (FObj (Functor⊗ Sets Sets MonoidalSets F) x)
+      φ x = Applicative.<*> mf  (FMap F (λ j k → (j , k))  (proj₁ x )) (proj₂ x)
+      _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b  
+      _<*>_  = Applicative.<*> mf  
+      comm00 : {a b :  Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b}  (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) →
+         (Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ ]) x ≡ (Sets [ φ o FMap (Functor● Sets Sets MonoidalSets F) f ]) x
+      comm00 {a} {b} {(f , g)} (x , y) = begin
+                 ( FMap (Functor⊗ Sets Sets MonoidalSets F) (f , g) ) ( φ (x , y) )
+             ≡⟨⟩
+                 FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ((FMap F (λ j k → j , k) x) <*> y)
+             ≡⟨ {!!} ⟩
+                 (FMap F (λ j k → f j , k)  x) <*> (FMap F g y)
+             ≡⟨ {!!} ⟩
+                 (FMap F (λ j k → j , k) (FMap F f x)) <*> (FMap F g y)
+             ≡⟨⟩
+                 φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
+             ∎ 
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+      comm0 : {a b : Obj (Sets × Sets)} { f : Hom (Sets × Sets) a b} → Sets [ Sets [ FMap (Functor⊗ Sets Sets MonoidalSets F) f o φ  ]
+        ≈ Sets [ φ  o FMap (Functor● Sets Sets MonoidalSets F) f ] ]
+      comm0 {a} {b} {f} =  extensionality Sets ( λ (x : ( FObj F (proj₁ a) * FObj F (proj₂ a)) ) → comm00 x )
+      comm10 :  {a b c : Obj Sets} → (x : ((FObj F a ⊗ FObj F b) ⊗ FObj F c) ) → (Sets [ φ  o Sets [ id1 Sets (FObj F a) □ φ  o Iso.≅→ (mα-iso isM) ] ]) x ≡
+                (Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o φ  □ id1 Sets (FObj F c) ] ]) x
+      comm10 {x} {y} {f} ((a , b) , c ) = begin
+                  {!!}
+               ≡⟨ {!!} ⟩
+                 {!!}
+             ∎
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+      comm1 : {a b c : Obj Sets} → Sets [ Sets [ φ 
+           o Sets [  (id1 Sets (FObj F a) □ φ ) o Iso.≅→ (mα-iso isM) ] ]
+        ≈ Sets [ FMap F (Iso.≅→ (mα-iso isM)) o Sets [ φ  o  (φ  □ id1 Sets (FObj F c)) ] ] ]
+      comm1 {a} {b} {c} =  extensionality Sets ( λ x  → comm10 x )
+      comm20 : {a b : Obj Sets} ( x : FObj F a * One )  → (  Sets [
+         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
+             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ) x  ≡ Iso.≅→ (mρ-iso isM) x
+      comm20 {a} {b} (x , OneObj ) =  begin 
+                 (FMap F (Iso.≅→ (mρ-iso isM))) ( φ ((  FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit))) (x , OneObj) ))
+               ≡⟨⟩
+                 FMap F proj₁ ((FMap F (λ j k → j , k) x) <*> (Applicative.pure mf OneObj))
+               ≡⟨ ≡-cong ( λ k → FMap F  proj₁ k) ( IsApplicative.interchange   ismf )  ⟩
+                 FMap F proj₁ ((Applicative.pure mf (λ f → f OneObj)) <*> (FMap F (λ j k → j , k) x))
+               ≡⟨ {!!} ⟩
+                 x
+               ≡⟨⟩
+                 Iso.≅→ (mρ-iso isM) (x , OneObj)
+             ∎ 
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+      comm2 : {a b : Obj Sets} → Sets [ Sets [
+         FMap F (Iso.≅→ (mρ-iso isM)) o Sets [ φ  o
+             FMap (m-bi MonoidalSets) (id1 Sets (FObj F a) , (λ _ → unit )) ] ] ≈ Iso.≅→ (mρ-iso isM) ]
+      comm2 {a} {b} =  extensionality Sets ( λ x  → comm20 {a} {b} x )
+      comm30 : {a b : Obj Sets} ( x : One * FObj F b )  → (  Sets [
+         FMap F (Iso.≅→ (mλ-iso isM)) o Sets [ φ  o
+             FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b) ) ] ] ) x  ≡ Iso.≅→ (mλ-iso isM) x
+      comm30 {a} {b} ( OneObj , x) =  begin 
+                 {!!}
+               ≡⟨ {!!} ⟩
+                 {!!}
+             ∎ 
+           where
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+      comm3 : {a b : Obj Sets} → Sets [ Sets [ FMap F (Iso.≅→ (mλ-iso isM)) o
+        Sets [ φ  o FMap (m-bi MonoidalSets) ((λ _ → unit ) , id1 Sets (FObj F b)) ] ] ≈ Iso.≅→ (mλ-iso isM) ]
+      comm3 {a} {b} =  extensionality Sets ( λ x  → comm30 {a} {b} x )
+
+
 
 HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
       ( unit  : FObj F One )