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.
This is a technical question about optics and coends. I'm going to paste in two relevant quotations from Riley's Categories of Optics and then ask my question.
on p. 3:
image.png
on p. 4:
image.png
This is then used to derive the nice graphical representation of optics as "diagrams with holes", aka comb elements.
This seems to rely on being small, in order for lemma 1.2.1 to apply, but typically we want to consider optics in categories like , or the Kleisli category of a probability monad, which are generally not small.
So I'm wondering how I should think about the string diagram calculus for optics in these non-small categories. Do we have to treat it as a sort of metaphorical thing (as in, it shows us how optics would behave if the category were small, but it's not, so we have to independently check all the results some other way), or is there some way that I can interpret diagrammatic proofs as correct even when is not small?
FinSet is "essentially small" : it's equivalent to a small category. So I would not worry about that case.
For the other examples, it's quite safe to assume your set, measure space, etc. has cardinality less than some inaccessible cardinal. If you do that - e.g., replace by the category of sets whose cardinality is for some inaccessible - you'll get a category that's essentially small. You can then replace by an equivalent small category and work with that. I bet everything will be fine and you'll never notice the difference.
This is just my first impression.
For what is worth, and as the official "coend guy" of profunctor optics ( :grinning: ) I have the same feeling as @John Baez that the solution is to either take a small category equivalent to the one you work with (when possible) or bound the size of the category from above in some way.
Thank you both. That makes a lot of sense, but also induces a sense of vertigo, because I never thought of myself as someone who would need to know anything about inaccessible cardinals. But it sounds like for most practical purposes I don't need to worry about it, at least for the time being.
Right, the point is that your "sets" could just as well be "sets in some set of sets that's so big you don't notice it's not the whole universe".
So, you really don't need to worry about it.
Something I didn't figure out until surprisingly recently is that if your base category is something like the kleisli category of a strong monad on a cartesian closed category (not 100% certain the exact conditions when it works), you can directly prove that the coend is isomorphic to a set:
Oh, that's really neat, thanks!
Me not knowing this earlier (or rather somebody did tell me but I never internalised it and then forgot) led to a huge amount of unnecessary work by my previous PhD student Joe Bolt in what is now the Bayesian Open Games paper. He figured out all the coend optics stuff before it became well known, and we could have just avoided optics entirely
I wonder if that also partially answers my other question here about Markov categories and optics, in the case where the Markov category is the Kleisli category of a monad with the right properties. That sort of looks like a stochastic map with the desired conditional independence property.
(These questions are partly inspired by reading the Bayesian Open Games paper, so this is good to know!)
Hmmm, could be...
There's an updated version of the paper that's under review but I think I didn't upload to arXiv yet. This fact is now in the paper, together with a post-hoc justification for overkilling it with coend calculus on the grounds that: 1) it's more general, 2) it matches the diagrams from Riley, which are still super useful, and 3) in the case of contexts (but not co/play maps!) the bound variable has a direct interpretation as the set of unobservable states of the game
Here's what I mean about the conditional independence thing. An element of is a thing that I give an to, and it gives me an together with something that I can give a and it will give me a . So the can depend on the and the , but the can only depend on the . It's not quite the same thing as a morphism with a conditional independence relation, but it seems like they ought to be isomorphic.