#
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).
|