# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1513005607 -32400
# Node ID 171f5386e87ee8f8afec49ed07212e6047f1ec2b
# Parent  01c618d942787470a281bddd677cc140258c24b5
Applicative→HaskellMonoidal begin

diff -r 01c618d94278 -r 171f5386e87e monoidal.agda
--- a/monoidal.agda	Mon Dec 11 23:43:52 2017 +0900
+++ b/monoidal.agda	Tue Dec 12 00:20:07 2017 +0900
@@ -979,3 +979,37 @@
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
 
+----
+--
+-- Applicative laws imples Monoidal laws
+--
+
+Applicative→HaskellMonoidal : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
+     ( pure  :  {a : Obj Sets} → Hom Sets a ( FObj F a ) )
+     ( <*> :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b   )
+     ( app : IsApplicative F pure <*> )
+       → IsHaskellMonoidalFunctor F (pure OneObj) (λ x →  <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x) )
+Applicative→HaskellMonoidal {l}  F pure <*> app = record {
+          natφ = natφ 
+        ; assocφ =  assocφ  
+        ; idrφ = idrφ 
+        ; idlφ = idlφ  
+   } where
+          unit  :  FObj F One
+          unit = pure OneObj
+          φ :  {a b : Obj Sets} → Hom Sets ((FObj F a) *  (FObj F b )) ( FObj F ( a * b ) )
+          φ = λ x →  <*> (FMap F (λ j k → (j , k)) ( proj₁ x)) ( proj₂ x)
+          isM  : IsMonoidal (Sets {l}) One SetsTensorProduct
+          isM = Monoidal.isMonoidal MonoidalSets
+          natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d  }
+             → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y)
+          natφ = {!!}
+          assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z }
+             → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (IsMonoidal.mα-iso isM)) (φ (φ (a , b) , c))
+          assocφ = {!!}
+          idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) (φ (x , unit)) ≡ x
+          idrφ = {!!}
+          idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) (φ (unit , x)) ≡ x
+          idlφ = {!!}
+
+