Mercurial > hg > Members > kono > Proof > category

diff freyd2.agda @ 830:232cea484067

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to CCC again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Mar 2020 14:26:39 +0900
parents 340708e8d54f
children
line wrap: on
line diff
--- a/freyd2.agda	Sat Jul 13 00:18:17 2019 +0900
+++ b/freyd2.agda	Sun Mar 15 14:26:39 2020 +0900
@@ -239,7 +239,7 @@
 
             
 
--- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable
+-- A is complete and K{*}↓U has preinitial full subcategory then U is representable (and U preserve Limit)
 
 -- if U preserve limit,  K{*}↓U has initial object from freyd.agda