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.
Ohad Kammar (Mar 26 2020 at 00:39):@Conor McBride hopefully we could do category theory in type theory soon.
Conor McBride (Mar 26 2020 at 00:43):That could be persuaded to suck a lot less, if we put our minds to it.
Ohad Kammar (Mar 26 2020 at 00:44):Do you have a roadmap? (beyond the Berlin talk)
Conor McBride (Mar 26 2020 at 00:58):It would be excessive to say I had a roadmap. I have some clues. E.g., I have a universe of presheaves-by-construction, but I seriously doubt it catches them all.
Ohad Kammar (Mar 26 2020 at 01:06):What about natural transformations? ;)
Nathanael Arkor (Mar 26 2020 at 01:08):@Ohad Kammar @Conor McBride: could you move this into another topic, so we can keep this topic for introductions? :)
Nathanael Arkor (Mar 26 2020 at 01:08):(you can move existing messages by editing them, and changing the topic)
Ohad Kammar (Mar 26 2020 at 01:09):Done! Ta
Nathanael Arkor (Mar 26 2020 at 01:09):thanks!
Conor McBride (Mar 26 2020 at 01:17):On the one hand, where's my free theorem? On the other hand, what's the normalisation-by-evaluation algorithm for definitional equalities up to free theorems? But that presupposes knowing which functions on objects lift to functors, and we're not there yet. Worse, our current setup forces us to discover that we have categorical structure post facto. We can't do it deliberately even if we know what we're doing. It's so frustrating!
Nathanael Arkor (Mar 26 2020 at 01:19):what was the topic of the Berlin talk?
Ohad Kammar (Mar 26 2020 at 01:26):https://icfp19.sigplan.org/details/tyde-2019-papers/17/Cubes-Cats-Effects
Ohad Kammar (Mar 26 2020 at 01:28):patty johann has a (new refinement) on this take, where every datatype remains a functor
Ohad Kammar (Mar 26 2020 at 01:30):But you said 'functions', not 'types', so maybe that won't help either.
Conor McBride (Mar 26 2020 at 01:47):I don't know what happened to the video from that talk. Maybe there were too many cartoons. Maybe I swore too much.
Conor McBride (Mar 26 2020 at 01:56):I said functions because coherence with respect to structure in small categories is hugely important. People who speak of "Hask" (the 'category' of Haskell types and functions) risk missing other categories at work in Haskell programming. We should write homomorphisms, not functions. And if the source has only discrete structure, we are none the worse off. At the moment, we don't even try to be rich.
Ohad Kammar (Mar 26 2020 at 01:59):Yes, that's what I meant when I asked about cats in TT.
And yes, functorial-by-construction is nice, but even if I was happy to do the legwork and prove functoriality manually, naturality is still a spanner
Reed Mullanix (Mar 26 2020 at 04:21):Shame that there is no video for the talk, that seems extremely interesting :slight_smile: If you don't mind me asking, are there slides available anywhere?
Conor McBride (Mar 26 2020 at 12:18):The slides were hand-drawn and presented "live" with cardboard animations, using my phone as a document camera. They're in my sketchbook, not in a file. Luckily, my sketchbook is in the same quarantine pod as me, so I could photograph the slides and put a (large) pdf somewhere, given time.
Max New (Mar 26 2020 at 13:09):@David Jaz is giving a talk on this topic today at the MIT categories seminar: http://brendanfong.com/seminar.html
Alex Kavvos (Mar 26 2020 at 14:31):That would be great. Which problems were you in particular trying to solve?
Alex Kavvos (Mar 26 2020 at 14:32):It is my understanding (though perhaps faulty) that Ali Caglayan and Mike Shulman have been working a lot on overcoming coherence issues in intensional TT. Something about threading coherence data through modules describing categories in Coq, I am told.
David Jaz (Mar 26 2020 at 15:29):Hi everybody!
In 30 minutes I'll be giving a talk for the MIT Categories Seminar. It will be an introduction to HoTT, geared towards people who use categories.
Cheers!
Jonathan Beardsley (Mar 26 2020 at 15:31):@David Jaz do you know if this will be recorded and available to watch later?
David Jaz (Mar 26 2020 at 15:33):It will be recorded and put on Youtube on the same channel.
James Fairbanks (Mar 26 2020 at 15:54):@David Jaz did you have a thread you wanted to do the chat in?
Alex Rice (Mar 26 2020 at 16:38):James Fairbanks said:
David Jaz did you have a thread you wanted to do the chat in?
It is under the MIT Categories Seminar stream
Beppe Metere (Mar 26 2020 at 17:34):Well... it was my first online attendance to a MIT Categories Seminar! Great job! Many thanks to the speaker and to the organizers! Beppe.
Mike Shulman (Mar 26 2020 at 18:22):I'd be happy to share something of what we're working on in the HoTT/Coq (with Ali as well as @Emily Riehl and others), but I don't quite know what entry point here people are interested in. E.g. exactly what coherence issues were you worried about? (I'm looking forward to watching David's talk too when the recording is posted.)
Faré (Mar 26 2020 at 19:11):What is the precise relationship between parametricity and naturality of transformations?
Nathanael Arkor (Mar 26 2020 at 19:13):there's a detailed exploration of parametricity (and naturality) in Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages (https://www.cs.bham.ac.uk/~udr/papers/logical-relations-and-parametricity.pdf)
Faré (Mar 26 2020 at 19:15):Thanks!
Valeria de Paiva (Mar 26 2020 at 19:39):hi, there is also older work, e.g. the thesis of Paola Maneggia in Birmingham on Parametricity and Linear Logic http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.121.9751&rep=rep1&type=pdf
Faré (Mar 26 2020 at 21:02):Ah, that reminds me of Computability Logic and its distinction between several universal quantifiers, including a "blinded" universal quantifier, that corresponds to Parametricity. Game Semantics FTW.
Faré (Mar 26 2020 at 21:02):But I'm not sure how THAT ties into Category Theory.
Dan Doel (Mar 28 2020 at 03:37):Section 6 of the Reynolds paper is giving me flashbacks to reading the notes about framed bicategories.
sarahzrf (Mar 28 2020 at 03:37):f r a m ed bi ca te gori e s :ghost:
sarahzrf (Mar 28 2020 at 03:38):who would frame a bicategory? for what crime?
Dan Doel (Mar 28 2020 at 03:39):For stealing the proarrow equipment.
Jacques Carette (Apr 24 2020 at 16:28):So apparently my pain threshold is way too high. I have not been too bothered with doing CT in Agda. Ok, once into Enriched land, type-checking is starting to be a bit sluggish, and debugging that is somewhat of a pain.
The current pain is trying to do Multicategories. Mainly because all human-mathematics presentations make copious use of "..." and depends in really crucial ways on the ordinal structure of the natural numbers (and taking that for granted, because that's baby mathematics). Formalizing that elegantly is my current challenge.
Agda wanted me to use 'subst' (aka transport) many many times. I refused its siren song - successfully. I'll write about that later, but the solutions all were imported from Partial Evaluation: if you don't want 'x + 0' to show up, then never write it down. You do that by using a 'sum' that internalizes its own properties, so has 3 cases instead of the naive 2 that a foldr-based implementation typically has.
eric brunner (Apr 24 2020 at 16:34):hott/coq ... i'll bite. i've read some of the literature and run the binaries a token number of times. rake++
Henry Story (Sep 26 2020 at 17:37):Hi, just wondering what people felt were the latest (best?) libraries to prove Category Theory structures using Proof Assistants?
I found this paper from 2014 by @David Spivak Experience Implementing a Performant Category-Theory Library in Coq.
And looking through this thread I found @David Jaz's HoTT type theory for doing Category Theory has been posted.
I'll go through those to going as a help to teach me to map between Category Theory and Type Theory. But would be interested to know what else people recognize now, 6 years later.
Henry Story (Sep 26 2020 at 22:23):I found the The HoTT library - a Formalization of Homotopy Type Theory in Coq. It is interesting to compare the HoTT book definitions with the implementation HoTT Coq Category library for example.
James Wood (Sep 26 2020 at 22:45):The library I'm most familiar with is agda-categories, by @Jacques Carette and contributors. It's done in plainish MLTT, and based on E-categories (that is, an ordinary category is a category enriched in setoids). I've found it to have a decent amount of stuff in it. The obvious drawback if you're interested in HoTT specifically is that the definitions are not made with HoTT in mind, so are likely to be inconvenient, or wrong if you care about equality.
Pedro Minicz (Sep 27 2020 at 18:06):@Scott Morrison made a small introduction for CT in Lean here.
Nikolaj Kuntner (Sep 27 2020 at 21:45):Thanks, will share.
Jacques Carette (Oct 01 2020 at 20:45):Jason and I wrote up our experience with writing agda-categories - see the web browsable version. We'll post an updated version of that paper once the embargo by the conference we've submitted to is lifted.