Mercurial > hg > Members > kono > Proof > category

diff list-monoid-cat.agda @ 168:a9b4132d619b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 20 Aug 2013 17:57:22 +0900
parents 744be443e232
children d6a6dd305da2
line wrap: on
line diff
--- a/list-monoid-cat.agda	Mon Aug 19 18:14:19 2013 +0900
+++ b/list-monoid-cat.agda	Tue Aug 20 17:57:22 2013 +0900
@@ -3,13 +3,7 @@
 open import HomReasoning
 open import cat-utility
 
-module free-monoid (c : Level ) where
-
-postulate A : Set
-
-postulate a : A
-postulate b : A
-
+module list-monoid-cat (c : Level ) where
 
 infixr 40 _::_
 data  List  (A : Set ) : Set  where
@@ -111,5 +105,3 @@
          ; isCategory = ( isMonoidCategory M )
           }
 
-
-