Mercurial > hg > Members > kono > Proof > category

diff discrete.agda @ 475:4c0a955b651d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add license
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 07 Mar 2017 12:31:35 +0900
parents 2d32ded94aaf
children 06388660995b
line wrap: on
line diff
--- a/discrete.agda	Tue Mar 07 08:27:33 2017 +0900
+++ b/discrete.agda	Tue Mar 07 12:31:35 2017 +0900
@@ -94,7 +94,7 @@
 
 record DiscreteObj  {c₁  : Level } (S : Set c₁) :  Set c₁  where
    field
-      obj : S
+      obj : S              -- this is necessary to avoid single object
 
 open DiscreteObj