--- a/nat.agda	Fri Jul 26 12:38:54 2013 +0900
+++ b/nat.agda	Fri Jul 26 15:52:24 2013 +0900
@@ -92,36 +92,27 @@
 
 open Kleisli
 -- η(b) ○ f = f
-Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
-                 { T : Functor A A }
-                 ( η : NTrans A A identityFunctor T )
-                 { μ : NTrans A A (T ○ T) T }
-                 { a : Obj A } ( b : Obj A ) 
-                 ( f : Hom A a ( FObj T b) )
-                 ( m : Monad A T η μ )
-                 { k : Kleisli A T η μ m}
-                      → A  [ join k (TMap η b) f  ≈ f ]
-Lemma7 c {T} η b f m {k} = 
-  let open ≈-Reasoning (c) 
-      μ = mu ( monad k )
-  in 
+Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) )
+                      → A  [ join K (TMap η b) f  ≈ f ]
+Lemma7 {_} {b} f = 
+  let open ≈-Reasoning (A) in 
      begin  
-         join k (TMap η b) f 
+         join K (TMap η b) f 
      ≈⟨ refl-hom ⟩
-         c [ TMap μ b  o c [ FMap T ((TMap η b)) o f ] ]  
-     ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
-        c [ c [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
-     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) )  ⟩
-        c [  id (FObj T b)   o f ]
-     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
+         A [ TMap μ b  o A [ FMap T ((TMap η b)) o f ] ]  
+     ≈⟨ IsCategory.associative (Category.isCategory A) ⟩
+        A [ A [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
+     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) )  ⟩
+        A [  id (FObj T b)   o f ]
+     ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩
         f
      ∎
 
 -- f ○ η(a) = f
-Lemma8 : ( a  : Obj A )  ( b : Obj A )
+Lemma8 : { a  : Obj A }  { b : Obj A }
                  ( f : Hom A a ( FObj T b) )
                       → A  [ join K f (TMap η a)  ≈ f ]
-Lemma8 a b f = 
+Lemma8 {a} {b} f = 
   begin
      join K f (TMap η a) 
   ≈⟨ refl-hom ⟩
@@ -139,11 +130,11 @@
 
 -- h ○ (g ○ f) = (h ○ g) ○ f
 Lemma9 : { a b c d : Obj A }
-                 ( f : Hom A a ( FObj T b) )
+                 ( h : Hom A c ( FObj T d) )
                  ( g : Hom A b ( FObj T c) ) 
-                 ( h : Hom A c ( FObj T d) )
+                 ( f : Hom A a ( FObj T b) )
                       → A  [ join K h (join K g f)  ≈ join K ( join K h g) f ]
-Lemma9 {a} {b} {c} {d} f g h = 
+Lemma9 {a} {b} {c} {d} h g f = 
   begin 
      join K h (join K g f)  
    ≈⟨⟩
@@ -197,9 +188,6 @@
      join K ( join K h g) f 
   ∎ where open ≈-Reasoning (A) 
 
-KHom1 :  (a : Obj A) → (b : Obj A)  -> Set (c₂ ⊔ c₁)
-KHom1 = {!!}
-
 record KHom (a : Obj A)  (b : Obj A)
      : Set (suc (c₂ ⊔ c₁)) where
    field
@@ -209,12 +197,10 @@
 K-id {a = a} = record { KMap =  TMap η a } 
 
 open import Relation.Binary.Core
+open KHom
 
-_⋍_ : 
-    { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ))
-_⋍_ = {!!}
-
-open KHom
+_⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ -- (suc ((c₂ ⊔ c₁) ⊔ ℓ))
+_⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
 _*_ : { a b : Obj A } → { c : Obj A } →
                       ( KHom b c) → (  KHom a b) → KHom a c 
@@ -228,6 +214,7 @@
                     ; associative = Kassoc
                     }
      where
+         open ≈-Reasoning (A) 
          isEquivalence :  { a b : Obj A } ->
                IsEquivalence {_} {_} {KHom a b} _⋍_
          isEquivalence {C} {D} =
@@ -236,20 +223,20 @@
              ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H}
              } where
                   ⋍-refl : {F : KHom C D} → F ⋍ F
-                  ⋍-refl = {!!}
+                  ⋍-refl = refl-hom
                   ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F
-                  ⋍-sym = {!!}
+                  ⋍-sym = sym
                   ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H
-                  ⋍-trans = {!!}
+                  ⋍-trans = trans-hom
          KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f
-         KidL = {!!}
+         KidL {_} {_} {f} =  Lemma7 (KMap f) 
          KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f
-         KidR = {!!}
+         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 = {!!}
          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 = {!!}
+         Kassoc {_} {_} {_} {_} {f} {g} {h} =  Lemma9 (KMap f) (KMap g) (KMap h)