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.
Adittya Chaudhuri (May 20 2025 at 05:48):If I am not misunderstanding, then, the discussion after Theorem 2.3 in the paper clearly stated that a cocartesian equipment is a stronger property of double categories than the property "symmetric monoidal".
I went through the defnition of an equipment (Definition A.2 here ) and its illustration there, and I found both the definition and the illustration very interesting (at least Mathematically).
If I understood correctly, I remember some months back @Evan Patterson explained me one of it's real world applications: namely capturing the subtypes of an influence type , which I find very interesting. However, I would also like to know about more possiblities of the real world applications of the stronger condition cocartesian equipment, and "why and how" the weaker condition "symmetric monoidal" is not sufficient/not nice for that purpose of that real world application?
Thanks in advance.
Kevin Carlson (May 20 2025 at 17:10):It’s a bit of a strange question. “Equipment” and “cocartesian” are orthogonal properties of a double category. I would never find myself going “oh geez, I thought I’d be able to get away with a symmetric monoidal double category here but I need [something] so I’d better upgrade to an equipment!”
Kevin Carlson (May 20 2025 at 17:15):In any case, I don’t think I know any direct applications of equipments to the real world. It’s much likelier to find yourself using objects of some equipment, like sets and relations, to model something in the world. You could also, similarly, imagine using an equipment as a flavor of double Lawvere theory whose models might then be systems of interest in the world; at least for implementation in software this has actually seemed like a bad idea, but finite product double theories have some of the restrictions required of an equipment, namely those along structure maps of products, and there are examples of those that get you kinds of models, such as Cartesian multicategories, you can’t get with plain Cartesian double theories. Cartesian multicategories are the natural semantics of nonlinear type theories, ie the type theories used implicitly or explicitly by all ordinary programming languages, so that’s one point of connection with an arguably “real” part of the world :smiling_face:
Adittya Chaudhuri (May 20 2025 at 19:30):Thank you!!
John Baez (May 20 2025 at 20:38):“Equipment” and “cocartesian” are orthogonal properties of a double category. I would never find myself going “oh geez, I thought I’d be able to get away with a symmetric monoidal double category here but I need [something] so I’d better upgrade to an equipment!”
I think Adittya was influenced something I claim @Evan Patterson said: a cocartesian equipment is an especially nice kind of symmetric monoidal category.
Adittya Chaudhuri (May 20 2025 at 20:39):I think yes :)
John Baez (May 20 2025 at 20:48):More precisely, two theorems from Structured and decorated cospans from the viewpoint of double category theory:
Let L : A → X be a functor into a category X with pushouts. Then the double category
of L-structured cospans is an equipment.
and
Suppose A is a category with finite coproducts, X is a category with finite colimits, and
L : A → X is a functor that preserves finite coproducts. Then the double category of L-structured cospans is cocartesian, hence also a cocartesian equipment.
John Baez (May 20 2025 at 20:49):add up to a strengthening of the old theorem that if A is a category with finite coproducts, X is a category with finite colimits, and L : A → X is a functor that preserves finite coproducts, then the double category of L-structured cospans is symmetric monoidal.