Mercurial > hg > Members > kono > Proof > category
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