changeset 724:df7697122d80

Free Theorem complete
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Nov 2017 10:59:38 +0900
parents 40122e9c7fc9
children bd371f36df9a
files monoidal.agda
diffstat 1 files changed, 17 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- 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