Mercurial > hg > Members > kono > Proof > category

changeset 988:d81341fad6e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 05 Mar 2021 10:55:45 +0900
parents 99c91423b871
children e1df57b34712
files src/yoneda.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/yoneda.agda	Fri Mar 05 10:20:20 2021 +0900
+++ b/src/yoneda.agda	Fri Mar 05 10:55:45 2021 +0900
@@ -302,10 +302,10 @@
 Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a))  (f : Hom A a b )
     → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
     → SetsAop [  g ≈ h ]
-Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A  (λ z → ( begin
-             TMap g _ z ≡⟨ {!!} ⟩
-             TMap g _ z ≡⟨ {!!} ⟩
-             TMap h _ z ∎ )) where  open ≡-Reasoning
+Yoneda-injective {a} {b} {x} {y} g h f yg=yh = begin
+             g   ≈⟨ {!!} ⟩
+             SetsAop [ {!!} o   SetsAop [ F2Nat f o g ] ] ≈⟨ {!!} ⟩
+             h  ∎  where  open ≈-Reasoning SetsAop
 
 -- full (surjective)
 Yoneda-surjective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop (FObj YonedaFunctor b) y) (f : Hom A a b )