Mercurial > hg > Members > kono > Proof > category

changeset 620:c95add5b7cbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 20 Jun 2017 22:44:09 +0900
parents 325ee3bef15c
children 19f31d22e790
files freyd2.agda
diffstat 1 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Tue Jun 20 22:36:15 2017 +0900
+++ b/freyd2.agda	Tue Jun 20 22:44:09 2017 +0900
@@ -209,13 +209,13 @@
                hom b (id1 A a ) o x
              ≈↑⟨ cdr ( ≡-≈ ( cong (λ k → k x ) (IsFunctor.identity (isFunctor (Yoneda A a))))) ⟩
                hom b (id1 A a ) o FMap (Yoneda A a) (id1 A a) x
-             ≈↑⟨ ≡-≈ ( cong (λ k → k x) (comm (id1 ((K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) (record { obj = obj b ; hom = ? } ) ))) ⟩
-                (Sets [ FMap (Yoneda A a) (arrow (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b)) o hom1 b ]) x
+             ≈⟨ {!!} ⟩
+               (Sets [ hom b o FMap (K Sets A (FObj (Yoneda A a) a)) (arrow (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b)) ]) x
+             ≈↑⟨ ≡-≈ ( cong (λ k → k x) (comm (id1 ((K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) b ))) ⟩
+               (Sets [ FMap (Yoneda A a) (arrow (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b)) o hom1 b ]) x
              ≈⟨⟩
-               arrow  (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b) o  hom1 b x
+               arrow  (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b) o  hom b x
              ≈⟨ idL ⟩
-               hom1 b x
-             ≈⟨ {!!} ⟩
                hom b x
              ∎ )
          initial0comm :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →