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.
Valeria de Paiva (Apr 29 2022 at 19:35):@Bruno Gavranovic can you copy here a bit of your GitHub directory https://github.com/bgavran/Lens_Resources that you think is most accessible to people who haven't seen any of this material before? Say only 3 references or thereabouts? Thanks in advance!!
Bruno Gavranović (Apr 29 2022 at 23:45):Absolutely. I'm actually trying to think about which of these resources has the most comprehensive and pedagogical introduction to lenses, and quite frankly I'm not sure :sweat_smile:
For lenses specifically, I believe Generalised Lens Categories is great. This includes monomorphic, bimorphic and dependent lenses, and various other exotic examples. Of course, dependent lenses are morphisms of polynomial functors, so all the Poly references might be useful as well.
For optics, one has Categories of Optics and Profunctor Optics: A Categorical Update. But all of these topics overlap with one another, and it depends what one's background is, and where one wants to go.
I think that I personally got the most mileage out of these three references.
It's also good to look at the applications section, or the blog post section in my github repo. I'd say that most of the papers in the application section present a very motivated view on lenses/optics, and they might be worth checking out. Likewise, sometimes the very readable way some of the blog posts are written can help with getting some intuitions before diving deep into the technical papers.
I shamelessly recommend some of my own posts for a very down-to-earth graphical way of thinking about lenses/optics :)
Jonathan Weinberger (Jun 02 2022 at 19:13):Does anyone have copy of Moss's thesis available currently? @Valeria de Paiva ? The Cambridge thesis portal is unavailable ATM
Valeria de Paiva (Jun 02 2022 at 19:41):Sorry Jonathan, I thought I had it but I had two copies of the LiCS paper instead, the title "The Dialectica Models of Type Theory" is the same.
Jonathan Weinberger (Jun 02 2022 at 19:45):Same @Valeria de Paiva but no worries, it should come back eventually
Valeria de Paiva (Jun 02 2022 at 19:46):but let me ask you, the model is the same as in the LiCS paper, isn't it? so why are you looking for Sean's thesis? I do have Tamara's thesis. do you?
Valeria de Paiva (Jun 02 2022 at 19:47):but indeed, very annoying to see the Cambridge repo down.
Jonathan Weinberger (Jun 02 2022 at 19:51):Yes, the model should be the same, but I've been looking more generally for some more elaborations on a couple of things; not top priority though
Jonathan Weinberger (Jun 02 2022 at 19:51):I think I do have Tamara's thesis FWIW
Valeria de Paiva (Jun 02 2022 at 19:57):Ok, I just sent you Sean's thesis, it was in my Dropbox connected to my old mac.
Jonathan Weinberger (Jun 02 2022 at 21:09):Great, thanks a lot @Valeria de Paiva
Jonathan Weinberger (Jun 02 2022 at 21:10):FWIW, Cambridge Apollo is back up now
Jonathan Weinberger (Jun 02 2022 at 21:10):https://www.repository.cam.ac.uk/handle/1810/280672
Valeria de Paiva (Jun 02 2022 at 21:11):typical, eh?
Charlotte Aten (Jun 03 2022 at 14:07):https://www.youtube.com/watch?v=4aGDCE6Nrz0
Nelson Niu (Jun 03 2022 at 16:31):764D2D82-3E6D-4310-AC9D-C9AE1549BC5C.jpg
Nelson Niu (Jun 03 2022 at 16:32):“lenses” seems like the right channel for photos
Valeria de Paiva (Jun 03 2022 at 16:36):Lovely @Nelson Niu ! the group looks great! very proud of you all for doing the MRC without me, you rock!! :revolving_hearts:
Bruno Gavranović (Jun 05 2022 at 19:42):Nelson Niu said:
Here's some of my photos, with a different set of people who are blinking/smiling :big_smile:
image.png
image.png
Jonathan Weinberger (Jun 20 2022 at 22:06):Not sure yet if (directly) relevant to us but I just saw that Bryce Clarke's thesis is now online, The Double Category of Lenses: https://t.co/PVab0D3Roo
Nelson Niu (Jun 20 2022 at 22:57):at one point I was considering whether Dialectica morphisms are squares in some appropriately defined double category but I didn’t get too far
Nelson Niu (Jun 20 2022 at 22:57):There’s almost certainly a generalization of the charts/lenses double category with for Dialectica though
Colin Bloomfield (Sep 08 2022 at 14:06):To get the Dialectica construction going on a category you need finite products and pullbacks so you can also get the contravariant sub-object functor. However, it seems that you just need products and a contravariant functor P into POS. I like this perspective because any intuitionistic first-order theory gives a free such functor P where its internal logic satisfies exactly T. Then one can take Dial(P) and then the objects are exactly (equivalence classes modulo T) of formulas (in context) p(u,x) and q(v,y) and morphisms are pairs of terms (I am simplifying, each could be a list of terms) (f(u), F(u,y)) such that p(u, F(u,y)) proves q(f(u), y) intuitionistically. Is this the generalization by Hyland? (Modulo using indexed categories instead of fibrations and partial orders instead of preorders) My apologies if this construction is being investigated by one of the groups (lenses?) and I am just catching up on basic definitions!
Update: I see this is in fact the generalization proposed by Hyland in "Proof Theory in the Abstract."