# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1377694319 -32400
# Node ID 173d078ee443d24da6e720d13a7e3f16dd6b9dcf
# Parent  d2d749318beecee85855bc564aba6c02c4a67d5f
Yoneda join

diff -r d2d749318bee -r 173d078ee443 yoneda.agda
--- a/yoneda.agda	Wed Aug 28 18:28:23 2013 +0900
+++ b/yoneda.agda	Wed Aug 28 21:51:59 2013 +0900
@@ -89,8 +89,33 @@
    isNTrans1 {a} = record { commute = refl  }
 
 _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c
-_+_  = {!!}
+_+_{a} {b} {c} f g  = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1  } where
+   commute1 :  (a b c : YObj ) (f : YHom  b c)  (g : YHom a b ) 
+            (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) →
+                        Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈
+                        Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ]
+   commute1  a b c f g a₁ b₁ h =   let open ≈-Reasoning (Sets {c₂})in begin
+                Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ]
+             ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩
+                Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] 
+             ≈⟨ car (nat f) ⟩
+                Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] 
+             ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩
+                Sets [ TMap f b₁ o Sets [ FMap b h  o TMap g a₁ ]  ]
+             ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩
+                Sets [ TMap f b₁ o Sets [ TMap g b₁  o FMap a h ]  ]
+             ≈↑⟨ assoc  {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h}  ⟩
+                Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] 
+             ∎ 
+   isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) 
+   isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h }
 
 isSetsAop :  IsCategory YObj YHom _≡_ _+_ Yid
-isSetsAop  =  {!!}
+isSetsAop  =  record  { isEquivalence =  ?
+                    ; identityL =   ?
+                    ; identityR =   ?
+                    ; o-resp-≈ =    ?
+                    ; associative = ?
+                    }
 
+