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.
Joshua Meyers (Feb 24 2024 at 17:54):Kind of a special case of this question by @Matteo Capucci (he/him) ...
I am trying to learn about double categories. It seems that most double categories that we care about in practice, e.g. , are actually weak double categories, i.e. pseudo categories internal to . I found the paper *Pseudo-Categories* by N. Martins-Ferreira, which gives a formal definition of these, along with pseudo functors and pseudo natural transformations between them. However, there are a lot of extremely involved coherences to even define these things, and what seems like way more involved coherences to check basic things like composition of pseudo functors giving a pseudo functor. I imagine that if I wanted then to begin to study "double category theory" just as I have studied "category theory", exploring the double categorical analogues for limits, adjunctions, Kan extensions, presheafs, profunctors, etc. every single step of the way would require checking a ton of coherences. It would probably move at least 10x slower than for category theory.
Of course there is the option to, every time I am confronted with a coherence, say "oh yeah it probably works out", and it seems that this is what most people do, but as @Amar Hadzihasanovic points out in the above question, category theory is full of cases where it actually doesn't work out.
So I don't know what to do. How do I enter into double category theory without either making unfounded assumptions that "it all works out" or spending hours checking coherences for every tiny step I want to make?
John Baez (Feb 24 2024 at 18:11):One thing you can do is get other people to check the coherence laws. You can get a grad student to do it...
... oh wait, you're a grad student, or at least you were. (Are you now?)
... or you can write papers with coauthors where you come up with theorems so delightful that they're willing to help out by checking the coherence laws.
Another thing you can do is use existing work to the maximum extent. There are various papers that provide "power tools" for working with double categories. For example, Mike Shulman's Framed bicategories and monoidal fibrations has let me avoid massive coherence law verifications. So - read the literature deeply and learn the state of the art!
John Baez (Feb 24 2024 at 18:13):Another thing you can do is build your own power tools. If you do this you may have to start by checking lots of coherence laws, but you'll prove theorems that can let you work at a higher level and not have to go down to the "machine code" of the fundamental definitions so often.
Joshua Meyers (Feb 24 2024 at 18:16):OK let's say I want to convince myself that weak double categories form a bicategory, or double category, or weak double category, or whatever they form. What are the power tools for that? The Martins-Ferreira paper has a whole bunch of scary coherences that look like they will take me a really long time to check.
Joshua Meyers (Feb 24 2024 at 18:17):I'm not currently a grad student, I just work part-time at Conexus now.
James Deikun (Feb 24 2024 at 18:19):This is an area where virtual double categories are surprisingly better than pseudo double categories. There's a lot of stuff you can prove about them at a high level by working with Cartesian monads. Monads have a much better-developed theory than pseudocategories.
Mike Shulman (Feb 24 2024 at 18:21):Not to necessarily disagree, but pseudo double categories are the algebras for a 2-monad, and you can get lots of mileage out of that. For instance, pseudo double categories form a 2-category because the algebras for any 2-monad form a 2-category.
Joshua Meyers (Feb 24 2024 at 18:23):Where can I read about this stuff?
John Baez (Feb 24 2024 at 18:23):Okay, yes Christian told me you work at Conexus but I wasn't sure if you'd left grad school.
OK let's say I want to convince myself that weak double categories form a bicategory, or double category, or weak double category, or whatever they form. What are the power tools for that?
I'd read Higher categories of double categories on the nLab, and then, since there's a shortage of references for details, I'd ask Mike Shulman where I can learn more details.
The Martins-Ferreira paper has a whole bunch of scary coherences that look like they will take me a really long time to check.
So you still think you need to check every step of a paper you're reading, even if the end result seems obvious? I.e. none of the work other people have done can save you from repeating that work? If this is your attitude I think you'll have to check a lot of coherence laws at some point, because often the way to get to a higher level of abstraction involves proving theorems where the proofs use a lower level of abstraction: you do grungy work at first so you don't have to do it later.
John Baez (Feb 24 2024 at 18:24):Joshua Meyers said:
Where can I read about this stuff?
I think you should be more specific, unless you're trying to get people to list lots of papers.
Joshua Meyers (Feb 24 2024 at 18:25):John Baez said:
Joshua Meyers said:
Where can I read about this stuff?
I think you should be more specific, unless you're trying to get people to list lots of papers.
I just meant the two suggestions, (1) of @James Deikun to look into virtual double categories and Cartesian monads, and (2) of @Mike Shulman to look into how pseudo double categories are the algebras for a 2-monad
John Baez (Feb 24 2024 at 18:26):Okay, they can answer those.
John Baez (Feb 24 2024 at 18:27):Obviously you should read the nLab articles [[double category]], [[virtual double category]] and lots of the papers in the references, but maybe there's more.
John Baez (Feb 24 2024 at 18:28):I think you should read lots of papers without verifying all results, just to get the "lay of the land".
James Deikun (Feb 24 2024 at 18:30):Well, the tutorial introduction to virtual double categories as Cartesian monads is Leinster's Higher operads, Higher Categories and then there's so much on monads in general I don't know where to begin, you're best off just searching for anything you think might be helpful for the stuff you're actually working on.
James Deikun (Feb 24 2024 at 18:32):I don't think @Joshua Meyers is talking about verifying the coherences being scary because he wants to verify the results, but rather because they're part of the definition of pseudocategory and the coherences need to hold when applying the results.
Mike Shulman (Feb 24 2024 at 18:32):For learning 2-monad machinery in general I would recommend Steve Lack's 2-categories companion. I don't know of somewhere that a construction of the 2-monad for pseudo double categories is written down explicitly, unfortunately, but I think that's true for many monads. The general machinery of presentations of monads ensures that it exists.
Joshua Meyers (Feb 24 2024 at 18:34):Thanks! I'll look into this stuff
John Baez (Feb 24 2024 at 19:20):James Deikun said:
I don't think Joshua Meyers is talking about verifying the coherences being scary because he wants to verify the results, but rather because they're part of the definition of pseudocategory and the coherences need to hold when applying the results.
When I last spoke to Joshua he wanted to personally verify all the theorems he used. At least that was my impression - maybe I got it wrong. But I think this is why he said:
I imagine that if I wanted then to begin to study "double category theory" just as I have studied "category theory", exploring the double categorical analogues for limits, adjunctions, Kan extensions, presheafs, profunctors, etc. every single step of the way would require checking a ton of coherences. It would probably move at least 10x slower than for category theory.
James Deikun (Feb 24 2024 at 19:27):Ah, that would certainly be laborious! :shock: Yeah, that's something to get over right quick. If someone really feels like shoring up the foundations, it would be much better to formalize a few of the theorems than to check them all by hand.
Kevin Arlin (Feb 25 2024 at 22:16):Yes, if you really wanted to verify everything you use I think that clearly implies that you want to work in a proof assistant and not on paper. Then at least other people as careful as you can rely on your stuff. New and Licata have a type theory for double categories; as far as I know it doesn’t interact with the main proof assistants, but I don’t know very far. https://maxsnew.com/docs/virtual-equipments.pdf
Brendan Murphy (Feb 25 2024 at 23:12):Oh this is very neat!
Brendan Murphy (Feb 25 2024 at 23:13):(also, if anyone is interested in formalizing double categories then please message me! I'm about to start working on adding them to mathlib)
Mike Shulman (Feb 25 2024 at 23:18):Double categories have recently been formalized in Coq UniMath: https://arxiv.org/abs/2402.05265. That may or may not be applicable to how you'll do it in Lean, though.
Brendan Murphy (Feb 25 2024 at 23:19):Yeah, I'm definitely going to take a look at that paper. But I expect the final product will end up pretty different in the absence of univalence
Brendan Murphy (Feb 25 2024 at 23:25):(and because mathlib's category theory library tries to design everything to play nicely with lean's simplifier & like everything in mathlib makes extensive use of type classes)
John Baez (Feb 25 2024 at 23:44):By the way, AlgebraicJulia relies pretty heavily on decorated and structured cospans for its epidemiological modeling software, which may also be repurposed for other modeling tasks. So far it doesn't treat those cospans using double categories. Mathematically speaking it 'should' - though one must always strike a balance between idealism and practicality. Luckily Evan Patterson, one of the main developers of AlgebraicJulia, is becoming an expert on double categories. So I'm hoping that eventually the AlgebraicJulia ecosystem will use double categories.
This is different than formalizing theorems about double categories: it's about putting the math of double categories to practical use. But that may boost interest in double categories, which could speed up getting their theory worked out well, and even getting it formalized. And eventually, if our civilization doesn't collapse first, the formalization could feed back to help the practical applications.
Kevin Arlin (Feb 26 2024 at 06:03):Double categories are also how one “should”/hopefully soon will be doing categorical database theory, for instance, to allow for both relational and functional database structures on an equal footing.
Max New (Feb 26 2024 at 14:44):Kevin Arlin said:
Yes, if you really wanted to verify everything you use I think that clearly implies that you want to work in a proof assistant and not on paper. Then at least other people as careful as you can rely on your stuff. New and Licata have a type theory for double categories; as far as I know it doesn’t interact with the main proof assistants, but I don’t know very far. https://maxsnew.com/docs/virtual-equipments.pdf
The type theory Dan and I developed is what I like to call a "domain-specific type theory". In theory some version might be implemented as an embedded DSL in a proof assistant but it's certainly not a trivial task to do so. Dan did make a kind of shallow embedding of the syntax in Agda so that we could get some machine-checked proofs but you can't instantiate them to prove things about, say some double category you construct in the proof assistant:
Kevin Arlin (Feb 26 2024 at 18:23):Thanks for the explanation Max. Do you have a particular vision about how so-called DSTTs would best be used?
Max New (Feb 26 2024 at 19:47):I do, and I should probably get to writing a grant about it...
Brendan Murphy (Feb 26 2024 at 20:18):I would really love to work on making edsl's in proof assistants easier to use. The only thoughts I've had towards this are to try and use Lean4's macro system to implement the "Type Systems as Macros" paper/the turnstile racket library, but it's not clear how this would handle integrating the host type system and the domain language type system
Max New (Feb 26 2024 at 21:28):You should probably talk to William Bowman: https://www.youtube.com/watch?v=vPYgzEdCxt8