Mercurial > hg > Members > kono > Proof > category

changeset 625:d73fbed639a9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initialObject done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 23 Jun 2017 21:43:09 +0900
parents 9b9bc1e076f3
children c5abbd39e6eb
files freyd2.agda
diffstat 1 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Fri Jun 23 21:20:10 2017 +0900
+++ b/freyd2.agda	Fri Jun 23 21:43:09 2017 +0900
@@ -228,6 +228,11 @@
          initial0 b = record {
                 arrow = hom b OneObj
               ; comm = comm1 b }
+         -- what is comm f ?
+         comm-f :  (b : Obj (K Sets A * ↓ (Yoneda A a))) (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
+            → Sets [ Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ]
+               ≈ Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ] 
+         comm-f b f = comm f
          unique : (b : Obj (K Sets A * ↓ Yoneda A a))  (f : Hom (K Sets A * ↓ Yoneda A a) initObj b)
                 → (K Sets A * ↓ Yoneda A a) [ f ≈ initial0 b ]
          unique b f = let open ≈-Reasoning A in begin
@@ -236,7 +241,9 @@
                 arrow f o id1 A a
              ≈⟨⟩
                 ( Sets [ FMap  (Yoneda A a) (arrow f) o id1 Sets (FObj (Yoneda A a) a)  ] ) (id1 A a)
-             ≈⟨ ≡-≈ ? ⟩
+             ≈⟨⟩
+               ( Sets [ FMap  (Yoneda A a) (arrow f) o ( λ x → id1 A a ) ] ) OneObj
+             ≈⟨ ≡-≈ ( cong (λ k → k OneObj ) (comm f )) ⟩
                ( Sets [ hom b  o  FMap  (K Sets A *) (arrow f) ]  ) OneObj
              ≈⟨⟩
                 hom b OneObj