# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511603372 -32400
# Node ID 69f01b82dfc917c844f92e80ee532724de87e449
# Parent  a8b595fb4905e6ccecbab23427a560a5422c16b8
uniquness of functor fmap

diff -r a8b595fb4905 -r 69f01b82dfc9 monoidal.agda
--- a/monoidal.agda	Sat Nov 25 16:40:17 2017 +0900
+++ b/monoidal.agda	Sat Nov 25 18:49:32 2017 +0900
@@ -553,23 +553,40 @@
       id x = x
       pure : {a : Obj Sets } → Hom Sets a ( FObj F a )
       pure a = Applicative.pure mf a
+      UniqunessOfFunctor :  {c₁ c₂ ℓ : Level} (C : Category c₁ c₂ ℓ) (F : Functor C C)
+          {a b : Obj C } { f : Hom C a b } → ( fmap :  Hom C a b → Hom C (FObj F a) ( FObj F b) )  → C [ fmap f ≈  FMap F f ]
+      UniqunessOfFunctor C F {a} {b} {f} fmap = begin  
+                fmap f 
+             ≈⟨ {!!} ⟩
+                FMap F f 
+             ∎ 
+           where
+                  open ≈-Reasoning C
+      pure→Fid : {a b : Obj Sets } → { f : a → b } → {x : FObj F a } →  FMap F id x ≡ pure id <*> x
+      pure→Fid {a} {b} {f} {x} = sym ( begin
+                 pure id <*> x
+             ≡⟨ IsApplicative.identity ismf  ⟩
+                 x
+             ≡⟨ ≡-cong ( λ k → k x ) (sym ( IsFunctor.identity (isFunctor F ) )) ⟩ FMap F id x
+             ∎ )
+           where
+                  open Relation.Binary.PropositionalEquality
+                  open Relation.Binary.PropositionalEquality.≡-Reasoning
       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
-             ≡⟨ {!!} ⟩
+             ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor Sets F ( λ f x → 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 (λ 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)