jamievicary
commented
6 years ago Hi Manuel, these are really superb ideas. The theoretical foundation of this first version of Globular has some limitations, and some colleagues and I have been developing a new approach to resolve them, within which working with functor categories is one of our main goals. Working with limits and colimits would also be an exciting goal which could be considered in this new approach, but many challenges remain in understanding both how they could be treated at a theoretical level (for example, the correct level of weakness to select), and how they could be yield a workable structure in an implementation.
On Mon, Feb 5, 2018 at 2:45 PM, Manuel Bärenz notifications@github.com wrote:
Often I feel like implementing some of my work in globular, and then I immediately stop because what I do isn't even supported (yet). If one could implement functors and their (co)limits, it would already increase the usefulness extraordinarily. I think this is maybe not too hard, so let me list the functionality that would be useful: Functors
Since all the categories globular are given by generators (and relations, which in turn are generators themselves), a functor really just amounts to choosing two previously specified categories, and a mapping of each k-cell generator in the source category onto a type-matching composition of k-cells in the target category. (Co)limits
It would be nice to flick on a switch on a given category to specify that it has (co)limits of a given shape. Then one should be able to use (co)limits whenever gluing together cells by just clicking a special button "insert (co)limit", and then specifying the functor over which to take the (co)limit.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/jamievicary/globular/issues/93, or mute the thread https://github.com/notifications/unsubscribe-auth/AKHHHnPfti1mgDpTY2MNF8A_boSZS9W2ks5tRxQGgaJpZM4R5jH2 .
Often I feel like implementing some of my work in globular, and then I immediately stop because what I do isn't even supported (yet). If one could implement functors and their (co)limits, it would already increase the usefulness extraordinarily. I think this is maybe not too hard, so let me list the functionality that would be useful:
Functors
Since all the categories globular are given by generators (and relations, which in turn are generators themselves), a functor really just amounts to choosing two previously specified categories, and a mapping of each k-cell generator in the source category onto a type-matching composition of k-cells in the target category.
(Co)limits
It would be nice to flick on a switch on a given category to specify that it has (co)limits of a given shape. Then one should be able to use (co)limits whenever gluing together cells by just clicking a special button "insert (co)limit", and then specifying the functor over which to take the (co)limit.