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.
Aaron David Fairbanks (Jan 23 2025 at 23:03):A few years ago, David Spivak wrote a paper called Functorial Aggregation, which was available on the arXiv. Now a new version by David, Richard Garner, and me is getting published! It's changed quite a lot from the older version.
The paper looks at various structures in the category of "single-variable polynomials": functors of the form (equivalently, parametric right adjoint functors ).
Something really neat and surprising, if you haven't seen it before, is Ahman and Uustalu's result that comonoids in (p.r.a. comonads on ) are categories.
However, it gets more interesting. We can consider "multi-variable polynomials" (p.r.a. functors for sets and ); and even more generally we can consider "polynomials with variables and values indexed by categories" (p.r.a. functors for categories and ). Extending Ahman and Uustalu's result, Richard pointed out in this video from 2019 that the framed bicategory of comonoids in (where 1-cells are bicomodules) is exactly the bicategory of these category-variable category-valued polynomials. A proof is given in the paper.
Not only the concept of a category but also the appropriate generalized concept of multi-variable polynomial fall right out of the concept of single-variable polynomial!
Kevin Carlson (Jan 24 2025 at 00:32):Congrats, looks great!
Jean-Baptiste Vienney (Jan 24 2025 at 01:28):Congrats @Aaron David Fairbanks !!
Aaron David Fairbanks (Feb 24 2025 at 04:59):A new paper, On Traces in Categories of Contractions by Peter Selinger and me appeared on the arXiv today! This version is twelve pages long, with some extra stuff in appendices. We plan to write a longer version later.
Here is the abstract:
Traced monoidal categories are used to model processes that can feed their outputs back to their own inputs, abstracting iteration. The category of finite dimensional Hilbert spaces with the direct sum tensor is not traced. But surprisingly, in 2014, Bartha showed that the monoidal subcategory of isometries is traced. The same holds for coisometries, unitary maps, and contractions. This suggests the possibility of feeding outputs of quantum processes back to their own inputs, analogous to iteration. In this paper, we show that Bartha's result is not specifically tied to Hilbert spaces, but works in any dagger additive category with Moore-Penrose pseudoinverses (a natural dagger-categorical generalization of inverses).
Moore-Penrose pseudoinverses are really interesting. They can be defined in any dagger category, and just like the definition of inverse, the definition of pseudoinverse is purely equational. When the pseudoinverse of an arrow exists, it is unique. They also arise very naturally in relation to idempotents -- an arrow is pseudoinvertible if and only if it constitutes some isomorphism of dagger-idempotents (where is basically projection onto the coimage of and is projection onto the image of ). Robin Cockett and @JS PL (he/him) wrote a very nice paper about pseudoinverses in 2023.
With pseudoinverses, one gets a generalized abstraction of "singular value decomposition" of arrows. This is what lets us prove the main result of our paper.
Aaron David Fairbanks (Jul 01 2025 at 04:54):Doubly weak double categories by me and @Mike Shulman has appeared on the arXiv!
Here is the abstract:
We propose a definition of double categories whose composition of 1-cells is weak in both directions. Namely, a doubly weak double category is a double computad -- a structure with 2-cells of all possible double-categorical shapes -- equipped with all possible composition operations, coherently. We also characterize them using "implicit" double categories, which are double computads having all possible compositions of 2-cells, but no compositions of 1-cells; doubly weak double categories are then obtained by a simple representability criterion. Finally, they can also be defined by adding a "tidiness" condition to the double bicategories of Verity, or to the cubical bicategories of Garner.
This collaboration started almost three years ago on this Zulip. It's the most ambitious project I have completed to date.
The results of the paper also include as a special case the "folklore" result that monoidal categories are equivalent to representable colored PROs. Some people here were interested in this, because it means non-strict monoidal categories are described directly by string diagrams. Just for the sake of it, here's a recap of that story:
A multicategory (a.k.a. virtual monoidal category) is a structure like a category but where each arrow has a list of input objects and one output object. A colored PRO (a.k.a., in the terminology of our paper, implicit monoidal category) is a structure like a category but where each arrow has a list of input objects and a list of output objects. It's the essentially algebraic structure that natively describes computations with string diagrams for monoidal categories.
A multicategory is called representable when all "tensor products" of lists of objects exist -- a tensor product being an object satisfying an appropriate universal property. It's well-known that monoidal categories may be equivalently described by representable multicategories, which is a definition of monoidal category that alleviates the need to deal with any coherence data. Moreover, a lax monoidal functor between monoidal categories is the same thing as a map between their underlying representable multicategories. (Multicategories are an essentially algebraic structure, and what is meant by a "map of multicategories" is a homomorphism of that structure.)
A colored PRO is likewise called representable when all "tensor products" of lists of objects exist. In this case tensor products are easier to define: a tensor product of a list of objects is simply an isomorphism to a single object. It's less well-known than the case of multicategories, but just as useful, that monoidal categories may be equivalently defined as representable colored PROs. A strong monoidal functor between monoidal categories is then the same thing as a map between the underlying representable colored PROs. (Colored PROs are an essentially algebraic structure, and what is meant by a "map of colored PROs" is a homomorphism of that structure.)
This generalizes from monoidal categories to bicategories. The analogous structures are then virtual 2-categories and (what we call) "implicit 2-categories". A lax functor of bicategories is the same as a map of underlying representable virtual 2-categories, and a pseudofunctor of bicategories is the same as a map of underlying representable implicit 2-categories. Our definition of doubly weak double category is then as a representable "implicit double category", and double pseudofunctors are then homomorphisms of the essentially algebraic structure.
There's a bunch of stuff in the paper, which I could blather on about, but I'll stop there. You can check it out!
Amar Hadzihasanovic (Jul 01 2025 at 07:09):Well done! And nice choice of terminology, I endorse it :)
Jacques Carette (Jul 01 2025 at 13:39):Nice. I wonder if that's equivalent to this definition. Which leads me to ask: have you formalized any of your work?
Aaron David Fairbanks (Jul 01 2025 at 16:15):Thanks for the link -- unfortunately I don't know Agda, but hopefully someone who does can chime in. Nothing has been formalized, but we did have interest in formalizing Section 8 in particular because it includes an especially fussy and subtle proof.
Jacques Carette (Jul 01 2025 at 16:29):I think your co-author is 'sufficiently fluent' in Agda. Basic idea is simple: in E-categories, you have the freedom to define what is equal to what. So you allow yourself to compose along morphisms that are 'equal' in the right way (not merely all equivalent morphisms).
This uses the "displayed algebra" approach.
Mike Shulman (Jul 01 2025 at 19:22):Thanks for the link Jacques. One obvious difference is that that's a definition of strict double categories in a setoidy world, rather than a definition of doubly weak double categories. There's obviously a connection and there are similar problems to deal with, but in the setoid case you don't care about treating the equalities of 1-cells as data, so for instance a double-bicategory-like definition would be just fine without needing any "tidiness".
Mike Shulman (Jul 01 2025 at 19:26):What's written there does look very much like such a double-bicategory-like approach, but with the "action" of bigons on squares replaced by a dependent equality. However, either I'm insufficiently fluent in Agda or there are a couple of aspects of that definition that seem wrong to me. Namely:
Frame≈ defines two squares to be equal if their boundaries are equal. Am I misreading that? Surely equality of squares should be a datum in addition to equality of their boundaries? Niels van der Weide (Jul 01 2025 at 22:48):Jacques Carette said:
Nice. I wonder if that's equivalent to this definition. Which leads me to ask: have you formalized any of your work?
There has been some recent work on formalizing weak double categories, see this paper and the formalization. This work builds forth upon the univalence principle paper (in particular, Example 9.3) and the formalization of pseudo double categories.
The notion of weak double category that we used in our formalization, is the same as what is used in Section 7 of the Doubly weak double categories paper. Specifically, we defined weak double categories as Verity double bicategories that satisfy a saturation conidition (see Definition 7.2 of our paper), and this saturation condition corresponds to their notion of tidiness.
Mike Shulman (Jul 01 2025 at 23:41):Ah, we should add a citation. Sorry about that -- I'd forgotten that you also mentioned the saturation/tidiness condition there.
Mike Shulman (Jul 02 2025 at 00:00):Why did you include explicit bigons in your definition? Was it just to align with the existing notion of double bicategory? I would expect that in a univalent type theory you could leave out the bigons and just say that you have horizontal and vertical (2,1)-categories, with hom-1-types. Then tidiness ought to be just be the univalence condition for 1-cells.
Jacques Carette (Jul 02 2025 at 01:09):The definitions in agda-categories are not 'principled' in a categorical sense, but quite speculative instead. They are instead the 'obvious' thing you get when you have absorbed setoidy thinking and dependent types (especially wrt equality) quite thoroughly. I've just never had anyone to discuss it with who understood all the subtleties to give a proper critique.
So I need to take some time to ponder your comments. Especially as I always considered setoidy as being 'naturally weak' (but in a bicategorical sort of way, indeed). So your comment that this is somehow strict came as quite the shock! Much thinking needed on my part.
Mike Shulman (Jul 02 2025 at 01:14):I mean, I suppose it depends on your perspective. I always think of setoids as standing in for sets, with the setoid "equality" standing in for equality of elements of a set. So an E-category is just as strict as a 1-category, with set(oid)s of morphisms and composition that is associative up to (setoid) equality rather than up to isomorphism.
Mike Shulman (Jul 02 2025 at 01:17):It's true that you could take a weak structure like a bicategory and regard it as an E-category, with the hom-setoids being the underlying groupoids of the hom-categories with their associativity and unitality forgotten. But in addition to forgetting associativity and unitality of composition of 2-cells, you'd be forgetting coherence for the associators and unitors of 1-cell composition, so I don't think it really makes sense to consider this as a weak structure. Rather, it's more like the homotopy 1-category of the bicategory, but where you've just neglected to actually take the quotient of the homotopy relation and kept it as setoids instead.
Jacques Carette (Jul 02 2025 at 01:24):It is likely quite perspective dependent. Since the same set of objects can have many different setoid structures, I see setoid equality as being 'programmable'. And lots of the work in agda-categories seemed to work much (much!) better when taking the weak perspective.
It'll take me a while to unpack your second paragraph.
(It's always worth remembering that I used E-categories not out of a philosophical conviction that they were 'right', but in fact as a desire to see where things would 'fail' to better understand how to design a good category theory library in MLTT. It just never really broke, much to my surprise. And that agda-categories was a playground for me and Jason to learn many things [success!] as well as a means to an end -- I really needed Rig Categories for some of my research!)
Mike Shulman (Jul 02 2025 at 01:26):What does "programmability" have to do with weakness?
Mike Shulman (Jul 02 2025 at 01:26):And what do you mean by "the weak perspective"?
Mike Shulman (Jul 02 2025 at 01:28):Category-theoretically, I think the right way to think of a setoid is as a locally contractible 2-groupoid. You might have many different equivalences between two objects, but they are all isomorphic to each other (and so you don't need to record those isomorphisms as data -- they just inform the setoidy perspective that you never care which "witness of equality" you're talking about).
Niels van der Weide (Jul 02 2025 at 09:39):Mike Shulman said:
Why did you include explicit bigons in your definition? Was it just to align with the existing notion of double bicategory? I would expect that in a univalent type theory you could leave out the bigons and just say that you have horizontal and vertical (2,1)-categories, with hom-1-types. Then tidiness ought to be just be the univalence condition for 1-cells.
One of our goals was to have a notion that encompasses both (univalent) pseudo double categories and (doubly) weak double categories.
Both pseudo double categories and weak double categories give rise to Verity double bicategories. However, there is a slight discrepancy: weak double bicategories give rise to a tidy/saturated Verity double bicategory, which is not the case for pseudo double categories. Let's say that pseudo double categories are strict in the vertical direction and weak in the horizontal direction. In this embedding, the vertical bigons/cells are taken to be identities of vertical morphisms, and those are not necessarily the same as squares. It is necessary to define the map this way, because otherwise univalence would not be preserved. In a univalent pseudo double category, we require the vertical category and the category of horizontal morphisms and squares to be univalent, but this is not sufficient to guarantee that the category of vertical morphisms and squares is univalent as well. For this reason, the notion of weak double category does not encompass the notion of pseudo double category, as pseudo double categories are only saturated/tidy in one direction. The notion of Verity double bicategory does give the desired framework, since we need the flexibility of having bigons/cells to encapsulate pseudo double categories as well. In our view, Verity double bicategories act as 'pre double categories'.
We can view this construction from the perspective of classical mathematics as well. There one can show that every pseudo double category gives rise to a weak double category in the obvious way. However, this construction does not interact well with equivalence. Specifically, vertical equivalence of pseudo double categories do not correspond to gregarious equivalence of their associated weak double category. Vertical morphisms are viewed up to equality in a horizontal equivalence, whereas they are viewed up to invertible squares in a gregarious equivalence. This construction would thus not be fully faithful in a suitable sense. If instead we map pseudo double categories to Verity double bicategories that are not fully saturated, then we obtain a construction that does interact well with vertical equivalences for weakly vertically invariant pseudo double categories (the cited paper uses horizontal invariance due to weakness being in the other direction).
Mike Shulman (Jul 02 2025 at 16:11):Wouldn't something like that also work with the framework I suggested? You don't need the noninvertible bigons for anything, and the invertible ones can be replaced by equalities, whether or not they are univalent/tidy/saturated. To distinguish the doubly-weak versus singly-weak, couldn't you just impose different univalence/nonunivalence conditions on the two directions, analogous to a univalent category and a strict category?
Ruby Khondaker (she/her) (Jul 09 2025 at 11:18):Hii, I skimmed through this paper and I really love the work you did! :D
I wanted to ask - is there a reason why you focused on an "algebraic" notion of a doubly weak double category? In terms of defining them as a special class of strict double categories (but in such a way that you can specify the 1-cells as the "generating 1-cells", and then compose appropriately).
Ruby Khondaker (she/her) (Jul 09 2025 at 11:21):E.g. as far as i can tell, for the fundamental double groupoid of X, the "actual" 1-cells are really continuous maps [0, n] -> X? So it seems similar to the sort of thing you do for the Moore path category, which has strict composites of paths.
Ruby Khondaker (she/her) (Jul 09 2025 at 11:22):so i guess you're relying on an algebraic notion of path composition that is strictly associative and unital, and you can do this by making sure the domain of the paths isn't just anymore?
Mike Shulman (Jul 09 2025 at 14:33):Are you talking about what we call the path double category of an implicit double category?
Intuitively, one should not really view those "composites" as existing at all. The definition of an implicit double category as a certain kind of strict double category is a quick way to get to a precise definition in section 3, but a more morally "correct" definition of implicit double category is given in section 5.
Ruby Khondaker (she/her) (Jul 09 2025 at 14:35):Mike Shulman said:
Are you talking about what we call the path double category of an implicit double category?
Intuitively, one should not really view those "composites" as existing at all. The definition of an implicit double category as a certain kind of strict double category is a quick way to get to a precise definition in section 3, but a more morally "correct" definition of implicit double category is given in section 5.
ah apologies, i was going off the definition in section 3, where you define an implicit double category as a strict one where the 1-cells are freely generated
Ruby Khondaker (she/her) (Jul 09 2025 at 14:36):ok so i see the section 5 definition - it's still "algebraic" but using the machinery of computads, if i understand correctly?
Ruby Khondaker (she/her) (Jul 09 2025 at 14:37):so actually, yes, i am talking about the path double category! the definition on page 33
Mike Shulman (Jul 09 2025 at 15:06):Yes, the point of the "real" definition in section 5 is that doubly weak double categories (and implicit double categories) are algebraic structure on double computads.
Ruby Khondaker (she/her) (Jul 09 2025 at 15:15):Mike Shulman said:
Yes, the point of the "real" definition in section 5 is that doubly weak double categories (and implicit double categories) are algebraic structure on double computads.
mhm mhm, of course. would it be possible to have instead a "geometric" definition of doubly weak double categories?
Mike Shulman (Jul 09 2025 at 16:44):In theory, certainly.
Mike Shulman (Jul 09 2025 at 16:44):Experience suggests that algebraic definitions are usually more convenient for .
Mike Shulman (Jul 09 2025 at 16:45):So that's what we wanted.
Ruby Khondaker (she/her) (Jul 09 2025 at 16:45):cool :)
Mike Shulman (Jul 09 2025 at 16:45):But it would be interesting to write down a geometric definition and compare them.
Ruby Khondaker (she/her) (Jul 09 2025 at 16:46):do you have an idea of how you'd go about doing it?
Ruby Khondaker (she/her) (Jul 09 2025 at 16:47):i guess you'd have to pick what shapes to use
Mike Shulman (Jul 09 2025 at 16:49):If you like simplicial sets as geometric shapes for 1-categories, the obvious choice to use for double categories is bisimplicial sets.
Ruby Khondaker (she/her) (Jul 09 2025 at 16:50):hm i would've thought cubical sets make sense here
Ruby Khondaker (she/her) (Jul 09 2025 at 16:50):they're squares after all, right?
Mike Shulman (Jul 09 2025 at 16:50):I think there's some work on "-double categories" out there somewhere, probably using bisimplicial sets, so one could just start from that and impose some kind of truncation condition.
Mike Shulman (Jul 09 2025 at 16:50):Bisimplicial sets also have a 2D square, .
Mike Shulman (Jul 09 2025 at 16:52):You could probably use cubical sets, but I think it would be trickier to formulate the filling conditions that way. The "natural" operations in a double category are composing two squares horizontally and vertically, which are represented in a bisimplicial set by and , but don't have an obvious representative in a cubical set. What kind of filling condition do you put on a 3D cube to indicate that it composes two 2D squares to another 2D square?
Notification Bot (Jul 09 2025 at 17:08):39 messages were moved from this topic to #learning: questions > algebraic vs geometric higher categories by Mike Shulman.
Aaron David Fairbanks (Jul 09 2025 at 17:51):Thanks for looking at our paper, Ruby, and for your kind words! As for your comment about the fundamental double groupoid, I'll also point out Proposition 7.22 and Example 7.23, where we give another (still algebraic) definition of doubly weak double category in terms of only square-shaped 2-cells, and we note that this can be used to quickly define the fundamental double groupoid.
Ruby Khondaker (she/her) (Jul 09 2025 at 18:09):Aaron David Fairbanks said:
Thanks for looking at our paper, Ruby, and for your kind words! As for your comment about the fundamental double groupoid, I'll also point out Proposition 7.22 and Example 7.23, where we give another (still algebraic) definition of doubly weak double category in terms of only square-shaped 2-cells, and we note that this can be used to quickly define the fundamental double groupoid.
Of course, thank you for writing such an awesome paper :D
Yes I see that part of the paper, it's cool that you both managed to figure out a fully algebraic definition! I've heard of this book called "nonabelian algebraic topology" which argues for using more cubical methods, including this double groupoid - apparently you get nonabelian analogs of the higher homotopy groups...?
Anyway I guess the only reason I'm more interested in "geometric" (or i guess "algebro-geometric") approaches myself is that they seem to be cleaner with regards to coherence conditions - e.g. for quasicategories, you don't need to explicitly supply any coherence isos or associators, they "come for free" in a sense.
I wonder how hard it'd be to generalise your work to 3-groupoids? I know that the homotopy 3-groupoid of is not equivalent to a strict one now, although I don't know enough higher category theory to tell whether this would prevent giving an algebraic definition in your style. The main thing I was worried about is that every implicit double category in your sense has a "strictification" given by its path category, so would a notion of "triply weak triple category" also have a strictification?
Ruby Khondaker (she/her) (Jul 09 2025 at 18:09):Apologies if these are silly questions by the way!
Mike Shulman (Jul 09 2025 at 18:29):Not silly at all. I don't know what the best definition of 3-category or triple category would be; the lack of a complete strictification would indeed be an issue.
In the globular case one could try using semistrictification and Gray-categories, e.g. define an implicit 3-category to be a ("path") Gray-category whose underlying [[sesquicategory]] is freely generated by a 2-computad. Or one could try to put algebraic structure on a 3-computad, but one would have to deal with the fact that naively defined 3-computads are not a presheaf category. Perhaps 3-diagrammatic sets would be a solution. And then one could try to generalize all of that to the triple case.
All of that seems like a lot of work, and possibly not worth the trouble. Dimension 3 is sort of the boundary point at which explicit algebraic structures are borderline-possible but very hard to deal with, and after that one generally has to reach for general tools like geometric shapes. (When I was a graduate student I remember Eugenia Cheng saying that the dimensions in higher category theory go "1, 2, lots, too many". That was before the big influx of homotopy theory to deal with higher dimensions.)
Ruby Khondaker (she/her) (Jul 09 2025 at 18:40):Mike Shulman said:
Not silly at all. I don't know what the best definition of 3-category or triple category would be; the lack of a complete strictification would indeed be an issue.
In the globular case one could try using semistrictification and Gray-categories, e.g. define an implicit 3-category to be a ("path") Gray-category whose underlying [[sesquicategory]] is freely generated by a 2-computad. Or one could try to put algebraic structure on a 3-computad, but one would have to deal with the fact that naively defined 3-computads are not a presheaf category. Perhaps 3-diagrammatic sets would be a solution. And then one could try to generalize all of that to the triple case.
All of that seems like a lot of work, and possibly not worth the trouble. Dimension 3 is sort of the boundary point at which explicit algebraic structures are borderline-possible but very hard to deal with, and after that one generally has to reach for general tools like geometric shapes. (When I was a graduate student I remember Eugenia Cheng saying that the dimensions in higher category theory go "1, 2, lots, too many". That was before the big influx of homotopy theory to deal with higher dimensions.)
could you just do a "geometric" definition of triply weak triple category, then?
Mike Shulman (Jul 09 2025 at 19:35):Probably, yes.