# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511595617 -32400
# Node ID a8b595fb4905e6ccecbab23427a560a5422c16b8
# Parent  13cef2bfa5c87cea6660a01f67b960cd9c6ac139
use  FMap F f x ≡ pure f <*> x

diff -r 13cef2bfa5c8 -r a8b595fb4905 monoidal.agda
--- a/monoidal.agda	Sat Nov 25 11:34:22 2017 +0900
+++ b/monoidal.agda	Sat Nov 25 16:40:17 2017 +0900
@@ -541,20 +541,58 @@
       _⊗_ 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 )
-      right : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
-      right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
       φ : {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  
+      left  :   {a b : Obj Sets} → {x y : FObj F ( a → b )} → {h : FObj F a  } → ( x ≡ y ) → x <*> h ≡ y <*> h
+      left {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k <*> h ) eq 
+      right  :   {a b : Obj Sets} → {h : FObj F ( a → b )} → {x y : FObj F a  } → ( x ≡ y ) → h <*> x ≡ h <*> y
+      right {_} {_} {h} {_} {_} eq = ≡-cong ( λ k → h <*> k ) eq 
+      id : { a : Obj Sets } → a → a 
+      id x = x
       pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
       pure a = Applicative.pure mf a
+      pure→F : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } →  FMap F f x ≡ pure f <*> x
+      pure→F {a} {b} {f} {x} = sym ( begin
+                 pure f <*> x
+             ≡⟨ {!!} ⟩
+                 FMap F f x
+             ∎ )
+           where
+                  open Relation.Binary.PropositionalEquality
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+
       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 (map f g) ((FMap F (λ j k → j , k) x) <*> y)
+             ≡⟨ {!!} ⟩
+                 (pure (map f g)) <*> ((pure (λ j k → j , k) <*> x) <*> y)
+             ≡⟨ sym ( IsApplicative.composition ismf )  ⟩
+                 (( pure _・_ <*> (pure (map f g))) <*> (pure (λ j k → j , k) <*> x)) <*> y
+             ≡⟨ left ( sym ( IsApplicative.composition ismf ))  ⟩
+                 ((( pure _・_ <*> (( pure _・_ <*> (pure (map f g))))) <*> pure (λ j k → j , k)) <*> x) <*> y
+             ≡⟨ {!!} ⟩
+                 (pure (( _・_ (( _・_ ((map f g))))) (λ j k → j , k)) <*> x) <*> y
+             ≡⟨⟩
+                (pure (λ j k → f j , g k) <*> x) <*> y
+             ≡⟨ {!!} ⟩
+                 ( pure ((_・_ (( _・_ ( ( λ h → h g ))) ( _・_ ))) ((λ j k → f j , k))) <*> x ) <*> y 
+             ≡⟨ {!!} ⟩
+                 (((pure  _・_ <*> (( pure  _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ ))) <*> (pure (λ j k → f j , k))) <*> x ) <*> y 
+             ≡⟨ left ( ( IsApplicative.composition ismf ))  ⟩
+                 ((( pure  _・_ <*> ( pure ( λ h → h g ))) <*> ( pure _・_ )) <*> (pure (λ j k → f j , k) <*> x )) <*> y 
+             ≡⟨  left (IsApplicative.composition ismf )  ⟩
+                 ( pure ( λ h → h g ) <*> ( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) ) <*> y 
+             ≡⟨ left (sym (IsApplicative.interchange ismf )) ⟩
+                 (( pure _・_ <*> (pure (λ j k → f j , k) <*> x )) <*>  pure g) <*> y 
+             ≡⟨  IsApplicative.composition ismf ⟩
+                 (pure (λ j k → f j , k) <*> x) <*> (pure g <*> y)
              ≡⟨ {!!} ⟩
                  (FMap F (λ j k → f j , k)  x) <*> (FMap F g y)
              ≡⟨  ≡-cong ( λ k → k  x <*> (FMap F g y)) ( IsFunctor.distr (isFunctor F ))  ⟩
@@ -563,6 +601,7 @@
                  φ ( ( FMap (Functor● Sets Sets MonoidalSets F) (f , g) ) ( x , y ) )
              ∎ 
            where
+                  open Relation.Binary.PropositionalEquality
                   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 ] ]
@@ -570,7 +609,7 @@
       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
-                  φ  (( id1 Sets (FObj F x) □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
+                  φ  (( id □ φ  ) ( ( Iso.≅→ (mα-iso isM) ) ((a , b) , c)))
                ≡⟨⟩
                  (FMap F (λ j k → j , k) a) <*> ( (FMap F (λ j k → j , k) b) <*> c)
                ≡⟨  sym (IsApplicative.composition  ismf) ⟩
@@ -647,11 +686,11 @@
           pure {a} x = FMap F ( λ y → x ) (unit )
           _<*>_ :   {a b : Obj Sets} → FObj F ( a → b ) → FObj F a → FObj F b        
           _<*>_ {a} {b} x y = FMap F ( λ r →  ( proj₁ r )  ( proj₂  r ) )  (φ ( x , y ))
-          -- left does not work right it makes yellows. why?
-          -- left : {n : Level} { a b : Set n} → { x y : a } { h : a → b }  → ( x ≡ y ) → h x ≡ h y
-          -- left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq 
-          right : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
-          right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
+          -- right does not work right it makes yellows. why?
+          -- right : {n : Level} { a b : Set n} → { x y : a } { h : a → b }  → ( x ≡ y ) → h x ≡ h y
+          -- right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq 
+          left : {n : Level} { a b : Set n} → { x y : a → b } { h : a }  → ( x ≡ y ) → x h ≡ y h
+          left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq 
           open Relation.Binary.PropositionalEquality
           FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d }
               { f : Hom Sets (c * d) e }
@@ -673,11 +712,11 @@
                   FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u
                ≡⟨  ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idlφ mono)) ⟩
                   FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mλ-iso isM)) ( φ ( unit , u) ) )
-               ≡⟨ right ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
+               ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
                   (FMap F ( (Iso.≅← (IsMonoidal.mλ-iso isM)) o   (Iso.≅→ (IsMonoidal.mλ-iso isM)))) ( φ ( unit , u) )
                ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( unit , u) )) (Iso.iso→ ( (IsMonoidal.mλ-iso isM) ))  ⟩
                   FMap F id ( φ ( unit , u) )
-               ≡⟨ right ( IsFunctor.identity ( isFunctor F ) ) ⟩
+               ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
                   id ( φ ( unit , u) )
                ≡⟨⟩
                   φ ( unit , u)
@@ -689,11 +728,11 @@
                   FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) u
                ≡⟨  ≡-cong ( λ k → FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) k ) (sym (IsHaskellMonoidalFunctor.idrφ mono)) ⟩
                   FMap F (Iso.≅← (IsMonoidal.mρ-iso isM)) ( FMap F (Iso.≅→ (IsMonoidal.mρ-iso isM)) ( φ ( u , unit ) ) )
-               ≡⟨ right ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
+               ≡⟨ left ( sym ( IsFunctor.distr ( isFunctor F ) )) ⟩
                   (FMap F ( (Iso.≅← (IsMonoidal.mρ-iso isM)) o   (Iso.≅→ (IsMonoidal.mρ-iso isM)))) ( φ ( u , unit ) )
                ≡⟨ ≡-cong ( λ k → FMap F k ( φ ( u , unit ) )) (Iso.iso→ ( (IsMonoidal.mρ-iso isM) ))  ⟩
                   FMap F id ( φ ( u , unit ) )
-               ≡⟨ right ( IsFunctor.identity ( isFunctor F ) ) ⟩
+               ≡⟨ left ( IsFunctor.identity ( isFunctor F ) ) ⟩
                   id ( φ ( u , unit ) )
                ≡⟨⟩
                   φ ( u , unit )
@@ -761,7 +800,7 @@
                      FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (Iso.≅← (mα-iso isM)) (φ (u , φ (v , w))))
                 ≡⟨⟩
                      FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (FMap F (λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) (φ (u , φ (v , w))))
-                ≡⟨ right (sym ( IsFunctor.distr (isFunctor F ))) ⟩
+                ≡⟨ left (sym ( IsFunctor.distr (isFunctor F ))) ⟩
                       FMap F (λ y → (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) ((λ r → (proj₁ r , proj₁ (proj₂ r)) , proj₂ (proj₂ r)) y )) (φ (u , φ (v , w)))
                 ≡⟨⟩
                      FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w)))
@@ -787,7 +826,7 @@
                         FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit)
                 ≡⟨⟩
                         FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit)
-                ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F ))) ⟩
+                ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F ))) ⟩
                         FMap F (λ y → f x) unit
                 ≡⟨⟩
                   pure (f x)
@@ -807,11 +846,11 @@
                   FMap F (λ r → proj₁ r x) (φ (u , unit))
               ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₁ r x) k ) φunitl ⟩
                   FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u )
-              ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩
+              ≡⟨ left ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩
                   FMap F (( λ r → proj₁ r x)  o ((Iso.≅← (mρ-iso isM) ))) u
               ≡⟨⟩
                   FMap F (( λ r → proj₂ r x)  o ((Iso.≅← (mλ-iso isM) ))) u
-              ≡⟨ right (  IsFunctor.distr (isFunctor F ))  ⟩
+              ≡⟨ left (  IsFunctor.distr (isFunctor F ))  ⟩
                   FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u)
               ≡⟨  ≡-cong ( λ k →  FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩
                   FMap F (λ r → proj₂ r x) (φ (unit , u))