# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511435889 -32400
# Node ID bc21e89cd273e12fbf4250a6a65341f10594e4ce
# Parent  5e101ee6dab95724fd973f3e26068ffdec32d391
...

diff -r 5e101ee6dab9 -r bc21e89cd273 monoidal.agda
--- a/monoidal.agda	Thu Nov 23 18:24:44 2017 +0900
+++ b/monoidal.agda	Thu Nov 23 20:18:09 2017 +0900
@@ -370,6 +370,13 @@
           law3 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x
           law4 : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x
 
+--   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
+-- naturality of φ       fmap(f × g)(φ u v) = φ ( fmap f u) ( fmap g v )
+-- left identity         fmap snd (φ unit v) = v
+-- right identity        fmap fst (φ u unit) = u
+-- associativity         fmap assoc  (φ u (φ v w)) = φ (φ u v) w
+
+
 record HaskellMonoidalFunctor {c₁ : Level} ( f : Functor (Sets {c₁}) (Sets {c₁}) )
         : Set (suc (suc c₁)) where
   field
@@ -480,6 +487,7 @@
   _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c
   _・_ f g = λ x → f ( g x ) 
   field
+          --   http://www.staff.city.ac.uk/~ross/papers/Applicative.pdf
           identity : { a : Obj Sets } { u : FObj f a } → pure ( id1 Sets a )  <*> u ≡ u
           composition : { a b c : Obj Sets } { u : FObj f ( b → c ) } { v : FObj f (a → b ) } { w : FObj f a }
               → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
@@ -525,6 +533,8 @@
         ; interchange = interchange
         }
      where 
+          id : { a : Obj Sets } → a → a 
+          id x = x
           isM  : IsMonoidal (Sets {c₁}) One SetsTensorProduct  
           isM = Monoidal.isMonoidal MonoidalSets 
           open IsMonoidal
@@ -536,16 +546,16 @@
           _・_ f g = λ x → f ( g x ) 
           identity : { a : Obj Sets } { u : FObj F a } → pure ( id1 Sets a )  <*> u ≡ u
           identity {a} {u} = begin 
-                 pure ( id1 Sets a )  <*> u
+                 pure id <*> u
                ≡⟨⟩
-                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id1 Sets a ) unit  , u ) )
-               ≡⟨  sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ ( FMap F ( λ y → id1 Sets a ) unit  ,  k u )))
+                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id ) unit  , u ) )
+               ≡⟨  sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ ( FMap F ( λ y → id ) unit  ,  k u )))
                     (  IsFunctor.identity ( Functor.isFunctor F ) ) ) ⟩
-                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id1 Sets a ) unit  , FMap F (id1 Sets a) u ) )
+                 ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) ( φ (  FMap F ( λ y → id ) unit  , FMap F id u ) )
                ≡⟨ sym ( ≡-cong ( λ k → ( FMap F ( λ a→b*b →  ( proj₁ a→b*b )  ( proj₂  a→b*b )) ) k  )  (  IsHaskellMonoidalFunctor.law1 mono  ) )  ⟩
-                   FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id1 Sets a) (λ x → x )) (φ (unit , u )))
+                   FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y → id) id) (φ (unit , u )))
                ≡⟨  ≡-cong ( λ k → k  (φ (unit , u ) )) ( sym ( IsFunctor.distr ( Functor.isFunctor F ) ) )  ⟩
-                   FMap F (λ x →  (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id1 Sets a) (λ x → x )) x )) (φ (unit , u ) )
+                   FMap F (λ x →  (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y → id) id) x )) (φ (unit , u ) )
                ≡⟨⟩
                    FMap F (λ x → proj₂ x ) (φ (unit , u ) )
                ≡⟨⟩
@@ -558,9 +568,33 @@
           composition : { a b c : Obj Sets } { u : FObj F ( b → c ) } { v : FObj F (a → b ) } { w : FObj F a }
               → (( pure _・_ <*> u ) <*> v ) <*> w  ≡ u  <*> (v  <*> w)
           composition {a} {b} {c} {u} {v} {w} = begin
-                  ?
-                ≡⟨  ? ⟩
-                 ?
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ y f g x → f (g x)) unit , u)) , v)) , w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u)) , FMap F id v)) , FMap F id w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                   (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (FMap F (map (λ y f g x → f (g x)) id ) (φ ( unit , u))) , FMap F id v)) , FMap F id w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                   (FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
+                ≡⟨⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ
+                   (FMap F ( λ y → (λ f g x → f (g x)) (proj₂ y ) ) (φ ( unit , u)) , FMap F id v)) , FMap F id w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (
+                   FMap F ( map (  λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) ( φ ( φ ( unit , u) , v))) , FMap F id w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
+                     FMap F ( λ x → (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) ((  map (  λ y → (λ f g x → f (g x)) (proj₂ y ) ) id ) x)) ( φ ( φ ( unit , u) , v))
+                       , FMap F id w))
+                ≡⟨⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (
+                     FMap F ( λ z → ((( λ f g x → f (g x)) (proj₂ (proj₁ z))) ( proj₂ z ))) ( φ ( φ ( unit , u) , v))
+                       , FMap F id w))
+                ≡⟨  {!!} ⟩
+                 FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (u , FMap F (λ a→b*b → proj₁ a→b*b (proj₂ a→b*b)) (φ (v , w))))
               ∎ 
            where
                   open Relation.Binary.PropositionalEquality.≡-Reasoning