# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1459037881 -32400
# Node ID 3fdf0aedc21d931fa5e0c8ec3257f09e6976fc23
# Parent  25478a0ba66bcec2846d4155f5debb6d903a508e
add discrete

diff -r 25478a0ba66b -r 3fdf0aedc21d limit-to.agda
--- a/limit-to.agda	Sat Mar 26 20:00:34 2016 +0900
+++ b/limit-to.agda	Sun Mar 27 09:18:01 2016 +0900
@@ -292,7 +292,7 @@
 record  Nil {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  :  Set   ( c₁ ⊔ c₂ ⊔ ℓ ) where
      field 
          nil : {a b : Obj A } → Hom A a b
-         nil-id : {a  : Obj A } →  A [ nil {a} {a} ≈ id1 A a ]
+         nil-id : {a  : Obj A } →  A [ nil {a} {a} ≈ id1 A a ]    -- too strong but we need this
          nil-idL : {a b c : Obj A } → { f : Hom A a b } → A [ A [ nil {b} {c} o f ]   ≈ nil {a} {c} ]
          nil-idR : {a b c : Obj A } → { f : Hom A b c } → A [ A [ f o nil {a} {b} ]   ≈ nil {a} {c} ]
 
@@ -493,7 +493,7 @@
                     ( nil none o  f ) o h 
                 ≈⟨ car ( nil-idL none ) ⟩
                      nil none  o h 
-                ≈⟨ car ( nil-id none ) ⟩
+                ≈⟨ car ( nil-id none ) ⟩ -- nil-id is need here
                      id1 A a  o h 
                 ≈⟨ idL ⟩
                      h