Mercurial > hg > Members > kono > Proof > category

changeset 723:40122e9c7fc9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
postulate Free Theorem
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 26 Nov 2017 10:41:21 +0900
parents 69f01b82dfc9
children df7697122d80
files monoidal.agda
diffstat 1 files changed, 23 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/monoidal.agda	Sat Nov 25 18:49:32 2017 +0900
+++ b/monoidal.agda	Sun Nov 26 10:41:21 2017 +0900
@@ -553,17 +553,8 @@
       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→Fid : {a b : Obj Sets } → (x : FObj F a ) →  FMap F id x ≡ pure id <*> x
+      pure→Fid {a} {b} x = sym ( begin
                  pure id <*> x
              ≡⟨ IsApplicative.identity ismf  ⟩
                  x
@@ -572,10 +563,30 @@
            where
                   open Relation.Binary.PropositionalEquality
                   open Relation.Binary.PropositionalEquality.≡-Reasoning
+      -----
+      -- they say it not possible prove FreeTheorem in Agda
+      --    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) )
+              → 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
       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 ) ) ⟩
+             ≡⟨ ≡-cong ( λ k → k x ) (UniqunessOfFunctor F ( λ f x → pure f <*> x ) ) ⟩
                  FMap F f x
              ∎ )
            where