--- a/nat.agda	Fri Jul 26 15:52:24 2013 +0900
+++ b/nat.agda	Fri Jul 26 16:18:32 2013 +0900
@@ -188,6 +188,20 @@
      join K ( join K h g) f 
   ∎ where open ≈-Reasoning (A) 
 
+Lemma10 :  {a b c : Obj A} -> (f g : Hom A a (FObj T b) ) → (h i : Hom A b (FObj T c) ) → 
+                          A [ f ≈ g ] → A [ h ≈ i ] → A [ (join K h f) ≈ (join K i g) ]
+Lemma10 {a} {b} {c} f g h i eq-fg eq-hi = let open ≈-Reasoning (A) in
+   begin 
+       join K h f
+   ≈⟨⟩
+       TMap μ c  o ( FMap T h  o f )
+   ≈⟨ cdr ( IsCategory.o-resp-≈ (Category.isCategory A) eq-fg ((IsFunctor.≈-cong (isFunctor T)) eq-hi )) ⟩
+       TMap μ c  o ( FMap T i  o g )
+   ≈⟨⟩
+       join K i g
+   ∎
+
+
 record KHom (a : Obj A)  (b : Obj A)
      : Set (suc (c₂ ⊔ c₁)) where
    field
@@ -199,7 +213,7 @@
 open import Relation.Binary.Core
 open KHom
 
-_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ -- (suc ((c₂ ⊔ c₁) ⊔ ℓ))
+_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
 _*_ : { a b : Obj A } → { c : Obj A } →
@@ -234,7 +248,7 @@
          KidR {_} {_} {f} =  Lemma8 (KMap f) 
          Ko-resp :  {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom  b c } → 
                           f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g)
-         Ko-resp = {!!}
+         Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = Lemma10 {a} {b} {c} (KMap f) (KMap g) (KMap h) (KMap i) eq-fg eq-hi
          Kassoc :   {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } →
                           (f * (g * h)) ⋍ ((f * g) * h)
          Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h)