--- a/nat.agda	Sun Jul 07 13:14:54 2013 +0900
+++ b/nat.agda	Sun Jul 07 16:38:48 2013 +0900
@@ -129,19 +129,25 @@
 
 open import Relation.Binary  renaming (Trans to Trans1 )
 open import Relation.Binary.Core  renaming (Trans to Trans1 )
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 module ≈-Reasoning where
 
   -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
   -- heterogeneous equalities, hence the code duplication here.                                                                         
 
-  trans : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}  {a b : Obj A } 
+  refl-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  {a b : Obj A } 
+                { x y z : Hom A a b }  →
+        A [ x ≈ x ]
+  refl-hom = \a -> IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory a ))
+
+  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 a b = {!!}
+  trans-hom = \a -> IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory a ))
 
   infix  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 ) :
@@ -152,11 +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 } 
+  _≈⟨_⟩_ : {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
-  _≈⟨_!_⟩_  = {!!}
---  _ ≈⟨_ x≈y ⟩ relTo y≈z = relTo (trans 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 {!!}