Mercurial > hg > Members > kono > Proof > category

changeset 619:325ee3bef15c

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:36:15 +0900
parents 23ff2464f7ad
children c95add5b7cbe
files freyd2.agda
diffstat 1 files changed, 10 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Tue Jun 20 16:36:01 2017 +0900
+++ b/freyd2.agda	Tue Jun 20 22:36:15 2017 +0900
@@ -198,6 +198,9 @@
            initial =  λ b → initial0 b
          ; uniqueness =  λ b f → unique b f
      } where
+         hom1 : (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → 
+                 Hom Sets (FObj (K Sets A (FObj (Yoneda A a) a)) (obj b)) (FObj (Yoneda A a) (obj b))
+         hom1 b = λ x → hom b x  
          initial0comm1 :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) → (x :  FObj (Yoneda A a) a )
             →  FMap (Yoneda A a) (hom b (id1 A a)) x ≡ hom b x
          initial0comm1 b x =  let open ≈-Reasoning A in ≈-≡ A ( begin
@@ -206,9 +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
-             ≈⟨ comm {!!} ⟩
-               FMap (K Sets A (FObj (Yoneda A a) a )) ? o hom 
-             ≈⟨ ? ⟩
+             ≈↑⟨ ≡-≈ ( 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
+             ≈⟨⟩
+               arrow  (id1 (K Sets A (FObj (Yoneda A a) a) ↓ Yoneda A a) b) o  hom1 b x
+             ≈⟨ idL ⟩
+               hom1 b x
+             ≈⟨ {!!} ⟩
                hom b x
              ∎ )
          initial0comm :  (b : Obj (K Sets A (FObj (Yoneda A a) a) ↓ (Yoneda A a))) →