Mercurial > hg > Members > kono > Proof > category

diff nat.agda @ 108:e763efd30868

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 21:02:32 +0900
parents 2feec58bb02d
children 5f331dfc000b
line wrap: on
line diff
--- a/nat.agda	Wed Jul 31 20:07:09 2013 +0900
+++ b/nat.agda	Wed Jul 31 21:02:32 2013 +0900
@@ -227,8 +227,7 @@
 _⋍_ : { a : Obj A } { b : Obj A } (f g  : KHom a b ) -> Set ℓ 
 _⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ]
 
-_*_ : { a b : Obj A } → { c : Obj A } →
-                      ( KHom b c) → (  KHom a b) → KHom a c 
+_*_ : { a b c : Obj A } → ( KHom b c) → (  KHom a b) → KHom a c 
 _*_ {a} {b} {c} g f = record { KMap = join K {a} {b} {c} (KMap g) (KMap f) }
 
 isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id