--- a/discrete.agda	Tue Mar 07 03:21:46 2017 +0900
+++ b/discrete.agda	Tue Mar 07 08:27:33 2017 +0900
@@ -101,7 +101,7 @@
 record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) 
       : Set c₁ where
    field
-      discrete : a ≡ b
+      discrete : a ≡ b     -- if f : a → b then a ≡ b
    dom : DiscreteObj S
    dom = a
 
@@ -125,7 +125,7 @@
     Obj  = DiscreteObj  {c₁} S ;
     Hom = λ a b →   DiscreteHom  {c₁} {S} a b  ;
     _o_ =  λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ;
-    _≈_ =  λ x y → dom x  ≡ dom y ;
+    _≈_ =  λ x y → dom x  ≡ dom y ;   -- x ≡ y does not work because refl ≡ discrete f is failed as it should be
     Id  =  λ{a} → DiscreteId a ;
     isCategory  = record {
             isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;