# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511327237 -32400
# Node ID 808b03184fd3452c0abb9566a99ee69674a7dd43
# Parent  dad072d52d0e00828c9e9a10da6790820e89731e
Applicative ⇔ Monoidal
  without commutative laws

diff -r dad072d52d0e -r 808b03184fd3 monoidal.agda
--- a/monoidal.agda	Wed Nov 22 12:49:17 2017 +0900
+++ b/monoidal.agda	Wed Nov 22 14:07:17 2017 +0900
@@ -331,6 +331,7 @@
   field
       pure  : {a : Obj Sets} → Hom Sets a ( FObj f a )
       <*>   : {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
+      --  should have Applicative law
 
 lemma1 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → Applicative f → HaskellMonoidalFunctor f
 lemma1 f app = record { unit = unit ; φ = φ }
@@ -339,13 +340,13 @@
      unit  :  FObj f One
      unit = pure app OneObj
      φ :  {a b : Obj Sets} → Hom Sets ((FObj f a) *  (FObj f b )) ( FObj f ( a * b ) )
-     φ {a} {b} ( x , y ) = <*> app {!!} {!!}
+     φ {a} {b} ( x , y ) = <*> app (FMap f (λ j k → (j , k)) x) y
 
 lemma2 : {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) ) → HaskellMonoidalFunctor f → Applicative f 
-lemma2 f app = record { pure = pure ; <*> = <*> }
+lemma2 f mono = record { pure = pure ; <*> = <*> }
   where
      open HaskellMonoidalFunctor
      pure  :  {a : Obj Sets} → Hom Sets a ( FObj f a )
-     pure {a} x = {!!} -- (unit app)
+     pure {a} x = FMap f ( λ y → x ) (unit mono)
      <*> :   {a b : Obj Sets} → FObj f ( a → b ) → FObj f a → FObj f b
-     <*> {a} {b} x = {!!}
+     <*> {a} {b} x y = FMap f ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b ) )  ( ** mono  x y  )