#
d0ecd297 |
|
02-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix category theory scripts in light of pat_assum rename
|
#
7106a911 |
|
09-Jan-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes to category theory example in light of 92317114
|
#
f76448c7 |
|
03-Jun-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
Update to category theory example. Main new result is a Yoneda embedding into the category of zfset-valued presheaves, whose properties are (mostly) simply inherited from the simpler embedding into the category of (predicate-)set-valued presheaves.
|
#
a3013634 |
|
19-May-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
More work on categoryTheory example Highlights include: - proof that an embedding is essentially injective on objects - one direction of the proof that an equivalence of categories is full, faithful, and essentially surjective on objects - proof that the binary product functor is a functor; characterization of binary products
|
#
65992c65 |
|
10-May-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
Major reworking of categoryTheory example Major changes include: - Reuse a polymorphic type of "morphisms" for morphisms in a category as well as for functors and natural transformations. The category record no longer has dom and cod fields. - Only store the id_map in a category (and the comp map) because the dom and cod of these morphisms is forced. - O'Keefe style treatment of the category of sets: have a separate category of sets for each HOL type (so really a subcategory of the real category of sets). Have not yet linked this up with a Katovsky-style zfset theory (would want to exhibit embeddings). - Use overloading and Parse rules for nicer syntax. - Split category theory into category, functor, and nat_trans theories. - Make many (all?) partial functions extensional, that is, explicitly set to ARB outside their domain (so that they are comparable). - Use the constants 'full' and 'faithful' and (new) 'inj_obj' to characterize the Yoneda embedding. Katovsky said it was injective on objects in "YonedaEmbedding", which is the wrong term. - Start a theory of limits (barely started).
|