Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: generalised lenses and generalised lens laws

Nathaniel Virgo (Sep 11 2021 at 11:10):

This is a vague question, I'm just wondering if anyone's thought about it or has any random insights.

There is a notion of "Generalised lenses" or "$F$-lenses" or "Grothendieck lenses", explained in David Spivak's Generalized Lens Categories via Functors $\mathscr{C}^\mathrm{op}\to \mathsf{Cat}$. This gives a very general notion of lens, but often it's desirable to impose some extra 'laws' on the lenses it produces.

Here are some examples:

• in a Cartesian category, if we take $F$ to be a particular functor that maps an object $X$ to the category of $X$-parametrised morphisms, then we obtain the usual category of lenses. However, depending on the application, it can be desirable to impose the traditional lens laws (PutGet, GetPut and PutPut) or some variation of them.

• In the paper linked above, Spivak obtains "dependent lenses" by taking $F$ to be a different functor. These dependent lenses are very closely related to polynomial functors, but, at least if I understood correctly, they're not quite the same. Polynomial functors are like dependent lenses that obey an additional law, given by the left-hand square in the diagram below, which is from David Spivak's Poly: An abundant categorical setting for mode-dependent dynamics

image.png

(I don't think this law arises automatically from the construction in the generalized lenses paper, but I could be wrong and I'm happy to be corrected if so.)

• In @Toby Smithe's work, e.g. Compositional Active Inference I: Bayesian Lenses. Statistical Games., we can take $F$ to be another functor to obtain a category of "Bayesian lenses". But it's sometimes useful to impose another law upon them to turn them into "exact Bayesian lenses."

I'm not 100% sure that all three of these "laws" are really the same kind of thing. But it seems striking and perhaps a bit unsatisfying that we can obtain lenses from a functor by performing this slick construction, but then having done that we often actually want a subcategory of the result, which has to be defined explicitly by adding these extra conditions. So I was wondering if there might be some deeper way to see where various kinds of laws we might want to impose come from. In other words, might there be some variation of the Grothendieck construction approach where not only the lenses but also their laws "pop out" of the construction in some way?

Matteo Capucci (he/him) (Sep 11 2021 at 13:00):

Construction 1 and 2 are exactly the same, dependent lenses do not satisfy an extra law

Matteo Capucci (he/him) (Sep 11 2021 at 13:04):

But you can add another example, similar to that of exact Bayesian lenses (and I suspect it's no coincidence): cartesian differential categories can be represented as subcategories of lenses, namely those lenses whose backward part is linear in a certain sense

Nathaniel Virgo (Sep 11 2021 at 14:20):

It was polynomial functors that I thought satisfied an extra law, rather than dependent lenses. Here's the description of dependent lenses from 'Generalised Lens Categories'

image.png

Polynomial functors fit this description but they also have to obey the extra law that this diagram commutes:

image.png

This is because in the polynomial functor case $f^\sharp$ can be thought of as a collection of functions mapping each fibre of $q\colon y\to d$ to a corresponding fibre of $p\colon x\to c$. Without this extra condition they can map to any element of $x$, not just the corresponding fibre of $p$.

Is it just that dependent lenses do also end up obeying this law as well? I haven't gone through all the details of deriving them from the Grothendieck construction yet, which is why I was a bit unsure about this example.

James Deikun (Sep 11 2021 at 18:05):

First of all this is a beautiful example of the microcosm principle. In Johnson, Rosebrugh and Wood's Lenses, fibrations and universal translations by we learn that we can see split Grothendieck (op)fibrations as categorified lenses, and here we learn that they are also categories of generalized prelenses.

Secondly, I have been thinking a lot about laws for "outlaw lenses" lately. This thinking is still in a state of flux, but it seems to be closely tied to what I am calling "secant categories". For a category $\mathcal{C}$, the secant category $S\mathcal{C}$ has

• as objects: pairs $(A,\mathcal{A})$ with $A$ an object of $\mathcal{C}$ and $\mathcal{A}$ an "$A$-colored monoid" -- an internal category whose object of objects must be $A$.
• as morphisms: pairs $(f, \mathcal{F})$ where $f$ is a function and $\mathcal{F}$ is a cofunctor with $f$ as its action on objects.

There is an obvious functor back to $\mathcal{C}$ that should be a fibration.

The normal lens laws for "very well-behaved lenses" or what I usually just call "lenses" come from the objects in this category that look like indiscrete categories and represent the notion of "an update is total replacement". There are a lot of other objects in this category though and they each give a notion of lens that respects the identity and composition in that object.

(I don't have the full list of references to hand, but if anyone ends up doing archaeology on this post, the notion of "secant category" was inspired by both tangent categories and the notion of "change structure" in the functional programming literature seen at, e.g. https://bentnib.org/posts/2015-04-23-incremental-lambda-calculus-and-parametricity.html )

(EDIT: It also occurs to me that I have heard something tangentially about someone claiming cofunctors as generalized lenses; it would be surprising if this didn't turn out to be the same insight as that.)

James Deikun (Sep 11 2021 at 18:07):

To relate it back, I think these laws will follow naturally when we see what the "update data" in the lens is being used for in each of these examples.

James Deikun (Sep 11 2021 at 20:26):

It seems that indeed Bryce Clarke (also on this server; not sure if I should ping or not) put these pieces together before I did:

• Clarke, Bryce. "Internal lenses as functors and cofunctors." arXiv preprint arXiv:2009.06835 (2020).

I can't seem to figure out the purpose of $f_1$ in Definition 19 (top of Section 4, the key definition of an internal lens), though; without it an internal lens reduces to merely a cofunctor, which seems neater.

Matteo Capucci (he/him) (Sep 12 2021 at 20:34):

Nathaniel Virgo said:

It was polynomial functors that I thought satisfied an extra law, rather than dependent lenses. Here's the description of dependent lenses from 'Generalised Lens Categories'

image.png

Polynomial functors fit this description but they also have to obey the extra law that this diagram commutes:

image.png

This is because in the polynomial functor case $f^\sharp$ can be thought of as a collection of functions mapping each fibre of $q\colon y\to d$ to a corresponding fibre of $p\colon x\to c$. Without this extra condition they can map to any element of $x$, not just the corresponding fibre of $p$.

Is it just that dependent lenses do also end up obeying this law as well? I haven't gone through all the details of deriving them from the Grothendieck construction yet, which is why I was a bit unsure about this example.

Yeah I'm pretty sure that's also satisfied by dependent lenses. The excerpt you mention doesn't state the commutativity condition again, but that's implied by their definition as a Grothendieck construction.

Matteo Capucci (he/him) (Sep 12 2021 at 20:34):

James Deikun said:

First of all this is a beautiful example of the microcosm principle. In Johnson, Rosebrugh and Wood's Lenses, fibrations and universal translations by we learn that we can see split Grothendieck (op)fibrations as categorified lenses, and here we learn that they are also categories of generalized prelenses.

This is very cool indeed!

Bryce Clarke (Sep 14 2021 at 23:26):

James Deikun said:

It seems that indeed Bryce Clarke (also on this server; not sure if I should ping or not) put these pieces together before I did:

• Clarke, Bryce. "Internal lenses as functors and cofunctors." arXiv preprint arXiv:2009.06835 (2020).

I can't seem to figure out the purpose of $f_1$ in Definition 19 (top of Section 4, the key definition of an internal lens), though; without it an internal lens reduces to merely a cofunctor, which seems neater.

The $f_1$ tells us that every morphism in the source category determines a morphism in the view category (rather than just on objects / states). This axiom really allows us to understand the Put action as a lift of morphisms. While there is lots one can do with cofunctors, (delta) lenses generally have much nicer properties (lots of research has been done in this direction, but there is still plenty to do!).

Bryce Clarke (Sep 14 2021 at 23:31):

Choosing between cofunctors and delta lenses really comes down to what level of generality you need. Both have a (forwards) assignment on objects. Cofunctors have a backwards lifting on morphisms, and delta lenses also have a forwards assignment on morphisms. It's worth mentioning that there are many nice relationships between delta lenses and cofunctors too; for example, in a recent paper I show it is possible to construct a cofree delta lens from every cofunctor.

James Deikun (Sep 14 2021 at 23:49):

Hm, there is certainly a use for being able to lower updates to the view as well as lifting them from it; but on the other hand cofunctors are much nicer objects in other ways as well, and for the project of bringing lawfulness to "bimorphic lenses" I'm not at all sure lowering updates is always possible over there. Having worked on FRP and incremental database views I can see how nice delta lenses would be in those particular applications though ...

James Deikun (Sep 15 2021 at 00:43):

One way to think about this that I'd just like to throw out there is: vectors push forward, forms pull back. If you think of a type as a space, then if your 'delta' is a vector the appropriate map is a functor, if it is a form your appropriate map is a cofunctor. If your type is a Riemannian space with an identification between vectors and forms via the metric, then wouldn't the appropriate map be something like a delta lens? This suggests there could be space for all three of these things in the world. (Though for functors there was never much danger ...)

Chad Nester (Apr 08 2022 at 12:34):

This seems as good a place to ask as any:

I'm looking for a citation to back up the assertion that "morphisms of polynomial functors are lenses". Is there a usual one?

Jules Hedges (Apr 08 2022 at 12:58):

The equivalence of categories between [polynomials, natural transformations] and [containers, morphisms of containers] appears first in whatever is the first paper on containers. Then you look at the definition of morphisms of containers and say "well, duh, it's the same as a lens"

Chad Nester (Apr 08 2022 at 13:46):

Hmm okay. Thanks.

Chad Nester (Apr 08 2022 at 13:47):

I might just shuffle this into an "among other things".

Chad Nester (Apr 08 2022 at 13:47):

I do have to read more about containers though :)