# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1511661578 -32400
# Node ID df7697122d80f6719fe558b9c6e6250151357f83
# Parent  40122e9c7fc9d4e9373c96eff8c78f35afd5a5fb
Free Theorem complete

diff -r 40122e9c7fc9 -r df7697122d80 monoidal.agda
--- a/monoidal.agda	Sun Nov 26 10:41:21 2017 +0900
+++ b/monoidal.agda	Sun Nov 26 10:59:38 2017 +0900
@@ -564,29 +564,32 @@
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
       -----
-      -- they say it not possible prove FreeTheorem in Agda
+      -- they say it not possible prove FreeTheorem in Agda nor Coq
       --    https://stackoverflow.com/questions/24718567/is-it-possible-to-get-hold-of-free-theorems-as-propositional-equalities
       --    and we cannot indent postulate ...
       postulate FreeTheorem : {l : Level } {a b c : Obj (Sets {l}) } → (F : Functor (Sets {l}) (Sets {l} ) ) →  ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) ) →  {h f : Hom Sets a b } →  {g k : Hom Sets b c } →  Sets [  g o h  ≈  k o f  ] →  Sets [ FMap F g o fmap h  ≈  fmap k o FMap F f  ]
       UniqunessOfFunctor :   (F : Functor Sets Sets)
           {a b : Obj Sets } { f : Hom Sets a b } → ( fmap : {a : Obj Sets } {b : Obj Sets } → Hom Sets a b → Hom Sets (FObj F a) ( FObj F b) )
+              → ( {b : Obj Sets } → Sets [ fmap  (id1 Sets b) ≈  id1 Sets (FObj F b) ] )
               → Sets [ fmap f ≈  FMap F f ]
-      UniqunessOfFunctor F {a} {b} {f} fmap =  extensionality Sets ( λ x → ( begin  
-                fmap f x
-             ≡⟨ {!!} ⟩
-                FMap F id ( ( fmap f  x ) )
-             ≡⟨  ≡-cong ( λ k → k x ) ( FreeTheorem F  fmap  ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory Sets ))) ) ⟩ 
-                fmap  id ( ( FMap F f x ) )
-             ≡⟨ {!!} ⟩
-                FMap F f x
-             ∎  ) )
-           where
-                  open Relation.Binary.PropositionalEquality
-                  open Relation.Binary.PropositionalEquality.≡-Reasoning
+      UniqunessOfFunctor F {a} {b} {f} fmap eq = begin
+                fmap f 
+             ≈↑⟨ idL ⟩
+                id1 Sets (FObj F b)  o  fmap f 
+             ≈↑⟨ car ( IsFunctor.identity (isFunctor F )) ⟩
+                FMap F (id1 Sets b)  o  fmap f 
+             ≈⟨ FreeTheorem F  fmap refl-hom ⟩ 
+                fmap  (id1 Sets b)  o  FMap F f  
+             ≈⟨ car eq ⟩
+                id1 Sets (FObj F b)  o  FMap F f  
+             ≈⟨ idL ⟩
+                FMap F f 
+             ∎  
+           where open ≈-Reasoning Sets hiding ( _o_ )
       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 F ( λ f x → pure f <*> x ) ) ⟩
+             ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor F ( λ f x → pure f <*> x ) ( extensionality Sets ( λ x →  IsApplicative.identity ismf  ))) ⟩
                  FMap F f x
              ∎ )
            where