Mercurial > hg > Members > kono > Proof > category
changeset 723:40122e9c7fc9
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