Mercurial > hg > Members > kono > Proof > category

changeset 434:3fdf0aedc21d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add discrete
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 27 Mar 2016 09:18:01 +0900
parents 25478a0ba66b
children 9f014f34b988
files limit-to.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- 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