--- a/HomReasoning.agda	Sat Aug 17 20:59:31 2013 +0900
+++ b/HomReasoning.agda	Sat Aug 17 21:08:33 2013 +0900
@@ -73,7 +73,6 @@
   sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
   sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))
 
-  sym-hom = sym
 -- How to prove this?
   ≡-≈ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≡ y ) → x ≈ y
   ≡-≈  refl = refl-hom
@@ -81,8 +80,8 @@
 --  ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : x ≈ y ) → x ≡ y
 --  ≈-≡  x≈y = irr x≈y
   ≡-cong : { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  →
-             (f : Hom B x y → Hom A x' y' )  → a ≡ b →  f a  ≈  f b
-  ≡-cong f refl =  ≡-≈ refl
+             a ≡ b  → (f : Hom B x y → Hom A x' y' ) →  f a  ≈  f b
+  ≡-cong refl f =  ≡-≈ refl
 
 --  cong-≈ :  { c₁′ c₂′ ℓ′ : Level}  {B : Category c₁′ c₂′ ℓ′} {x y : Obj B } { a b : Hom B x y } {x' y' : Obj A }  → 
 --             B [ a ≈ b ] → (f : Hom B x y → Hom A x' y' ) →  f a ≈ f b
@@ -116,7 +115,7 @@
       →   A [ A [ FMap G f  o  TMap η a ]  ≈ A [ TMap η b  o  FMap F f ] ]
   nat η  =  IsNTrans.commute ( isNTrans η  )
 
-  infixr 2 _∎
+  infixr  2 _∎
   infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
   infix  1 begin_
 
@@ -136,20 +135,12 @@
            x ≈ y → y IsRelatedTo z → x IsRelatedTo z
   _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
 
-
-  _≈↑⟨_⟩_  : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
-           y ≈ x → y IsRelatedTo z → x IsRelatedTo z
-  _≈↑⟨_⟩_ _  x≈y (relTo y≈z) = relTo (trans-hom (sym x≈y) y≈z)
-
-  infixr 2 _≈↑⟨_⟩_ 
-
   _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
   _ ≈⟨⟩ x∼y = x∼y
 
   _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
   _∎ _ = relTo refl-hom
 
-
 -- an example
 
 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →