You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Henri Tuhola (Apr 24 2020 at 15:31):It looks interesting. I'm writing about CAM this weekend anyway. It overlaps a lot with normalization-by-evaluation, also the normal form is suitable for building a proof search engine.
But maybe the thing why I came up here is because I wonder how people think about type classes in category theory?
Henri Tuhola (Apr 24 2020 at 15:34):Starting by denotational semantics of type classes, they'd seem to be implicit parameters and relate a lot with modules and abstract datatypes.
(=_=) (Apr 24 2020 at 15:36):Henri Tuhola said:
But maybe the thing why I came up here is because I wonder how people think about type classes in category theory?
That'd be a good topic for #practice: programming.
Henri Tuhola (Apr 24 2020 at 15:41):I'll try to think of a title for the post. But maybe that's the hard part because if I knew how to title it, then I'd already know the answer to my own question. Maybe I just have to put "what are typeclasses in category theory?" or similar.
Henri Tuhola (Apr 24 2020 at 15:42):If polymorphic functions are like natural transformations, and functors are like types, typeclasses are like?
(=_=) (Apr 24 2020 at 15:55):I started a new topic, #practice: programming > type classes, for anyone who's interested in continuing this conversation.
Nikolaj Kuntner (Jun 01 2020 at 00:29):According to this MO thread, the Axiom of Replacement is needed for at least some constructions, such as (cardinally larger) (co-)limits and, as discussed in the comments of the question, also bigger functor categories
https://mathoverflow.net/questions/41118/axiom-of-replacement-in-category-theory
This makes me wonder about Mac Lane set theory, which has less tools at hand than Z, which has no F (Frannkels Replacement).
Does this say some of those constructions are generally not available in those theories (and the corresponding topoi). E.g. if you want to investigate bigger objects in functor categories. Or maybe it does depend on the coding?
(PS this is not about CS kind of classes per se, but I didn't find a better suited channel.)
edit: Moved to "general / Axiom systems"
John Baez (Jun 01 2020 at 00:45):Btw it's super-easy to make up new channels for any topic you want, and probably good to do. You can even do it retroactively, like now.
(=_=) (Jun 01 2020 at 06:26):Nikolaj Kuntner said:
edit: Moved to "general / Axiom systems"
That's #theory: logic > Axiom systems, for anyone who's confused.