--- a/nat.agda	Sun Jul 07 16:38:48 2013 +0900
+++ b/nat.agda	Sun Jul 07 18:16:46 2013 +0900
@@ -144,10 +144,10 @@
   trans-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } 
                 { x y z : Hom A a b }  →
         A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
-  trans-hom = \a -> IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory a ))
+  trans-hom a b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory a ))) b c
 
-  infix  2 _∎
-  infixr 2 _≈⟨_⟩_ 
+  infixr  2 _∎_
+  infixr 2 _≈⟨_!_⟩_ 
   infix  1 begin_
 
   data IsRelatedTo  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } ( x y : Hom A a b ) :
@@ -158,16 +158,13 @@
            IsRelatedTo A x y → A [ x ≈ y ]
   begin relTo x≈y = x≈y
 
-  _≈⟨_⟩_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}  {a b : Obj A } 
-                { x y z : Hom A a b } →
-           A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z
-  _≈⟨_⟩_ = {!!}
+  _≈⟨_!_⟩_ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->  {a b : Obj A }
+                ( x : Hom A a b ) → { y z : Hom A a b } → 
+                A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z
+  a ≈⟨ _ !  x≈y ⟩ relTo y≈z  = relTo ( trans-hom a x≈y y≈z )
 
---   _≈⟨ x ⟩ _ = ? -- relTo (Trans1 x≈y y≈z)
---   _≈⟨ x≈y ⟩ relTo y≈z = ? -- relTo (Trans1 x≈y y≈z)
-
-  _∎ :  {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
-  _∎ _ = relTo {!!}
+  _∎_ :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
+  a ∎ _ = relTo ( refl-hom a )
 
 open Kleisli
 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->