Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
829:6c5cfb9b333e 830:232cea484067
237 hom b OneObj 237 hom b OneObj
238 ∎ 238 ∎
239 239
240 240
241 241
242 -- A is complete and K{*}↓U has preinitial full subcategory and U preserve limit then U is representable 242 -- A is complete and K{*}↓U has preinitial full subcategory then U is representable (and U preserve Limit)
243 243
244 -- if U preserve limit, K{*}↓U has initial object from freyd.agda 244 -- if U preserve limit, K{*}↓U has initial object from freyd.agda
245 245
246 ≡-cong = Relation.Binary.PropositionalEquality.cong 246 ≡-cong = Relation.Binary.PropositionalEquality.cong
247 247