Mercurial > hg > Members > kono > Proof > category

changeset 187:47d6a9bc3933

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hint
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2013 00:54:15 +0900
parents b2e01aa0924d
children f4c9d7cbcbb9
files yoneda.agda
diffstat 1 files changed, 11 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/yoneda.agda	Wed Aug 28 23:32:24 2013 +0900
+++ b/yoneda.agda	Thu Aug 29 00:54:15 2013 +0900
@@ -164,10 +164,17 @@
          FObj = λ a → CF {a}
        ; FMap = λ f → y-nat f
        ; isFunctor = record {
-             identity =  {!!}
-             ; distr = {!!}
-             ; ≈-cong = {!!}
+             identity =  identity
+             ; distr = distr1
+             ; ≈-cong = ≈-cong
         } 
-  }
+  } where
+        ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-nat f ≈ y-nat g ]
+        ≈-cong {a} {b} {f} {g} eq = {!!} -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [  g o  g₁ ] )
+        identity : {a : Obj A} → SetsAop [ y-nat (id1 A a) ≈ id1 SetsAop (CF {a} )  ]
+        identity  {a} = {!!} -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x)
+        distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-nat (A [ g o f ]) ≈ SetsAop [ y-nat g o y-nat f ] ]
+        distr1 {a} {b} {c} {f} {g} = {!!} -- (λ x g₁ → (A [  (A [ g o f]  o g₁ ]) ≡ (λ x x₁ → A [  g .o A [ f o x₁ ] ] )
 
 
+