--- a/maybeCat.agda	Sun Mar 20 11:36:44 2016 +0900
+++ b/maybeCat.agda	Sun Mar 20 12:32:13 2016 +0900
@@ -30,17 +30,17 @@
 _[_≡≡_]  A =  Eq ( Category._≈_ A ) 
 
 
-*refl :   { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
-*refl  {_} {_} {_} {A} {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
-*refl  {_} {_} {_} {A} {_} {_} {nothing} = nothing
+≡≡-refl :   { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } ->  {a b : Obj A } -> {x : Maybe ( Hom A a b ) } → A [ x ≡≡ x ]
+≡≡-refl  {_} {_} {_} {A} {_} {_} {just x}  = just refl-hom where  open ≈-Reasoning (A)
+≡≡-refl  {_} {_} {_} {A} {_} {_} {nothing} = nothing
 
-*sym :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ x ]
-*sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
-*sym {_} {_} {_} {A} nothing    = nothing
+≡≡-sym :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ x ]
+≡≡-sym {_} {_} {_} {A} (just x≈y) = just (sym x≈y)  where  open ≈-Reasoning (A)
+≡≡-sym {_} {_} {_} {A} nothing    = nothing
 
-*trans :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
-*trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
-*trans {_} {_} {_} {A} nothing    nothing    = nothing
+≡≡-trans :  { c₁ c₂ ℓ : Level} -> { A : Category c₁ c₂ ℓ } -> {a b : Obj A } -> {x y z : Maybe ( Hom A a b ) }  → A [ x ≡≡ y ] → A [ y ≡≡ z ] → A [ x ≡≡ z ]
+≡≡-trans {_} {_} {_} {A} (just x≈y) (just y≈z) = just (trans-hom x≈y y≈z)  where  open ≈-Reasoning (A)
+≡≡-trans {_} {_} {_} {A} nothing    nothing    = nothing
 
 
 
@@ -52,7 +52,7 @@
     _≈_ = λ a b →    _[_≡≡_] { c₁} {c₂} {ℓ} A  (hom a) (hom b)  ;
     Id  =  \{a} -> MaybeHomId a ;
     isCategory  = record {
-            isEquivalence = record {refl = *refl  {_} {_} {_} {A}; trans = *trans  {_} {_} {_} {A}; sym = *sym  {_} {_} {_} {A}};
+            isEquivalence = record {refl = ≡≡-refl  {_} {_} {_} {A}; trans = ≡≡-trans  {_} {_} {_} {A}; sym = ≡≡-sym  {_} {_} {_} {A}};
             identityL  = \{a b f} -> identityL {a} {b} {f} ;
             identityR  = \{a b f} -> identityR {a} {b} {f};
             o-resp-≈  = \{a b c f g h i} ->  o-resp-≈ {a} {b} {c} {f} {g} {h} {i} ;