Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Someone left a query at bicategory of relations, and I put down a partial response (proving the separability condition). I plan to add a little more later, but I confess that I don’t see how to derive the other dual Frobenius condition from the one given. (Hard to believe the dual one wasn’t given by Carboni and Walters.)
Carboni and Walters call a “bicategory of relations” a discrete cartesian bicategory (because the local posets of maps are discrete). They are equivalent to unitary pretabular allegories.
Okay, I’ve figured out the derivation of the dual Frobenius condition, and I’ll get to it in a bit.
That was me; sorry I didn’t sign the query. Thank you!
Okay, I’ve added a good chunk of material to the article, leading up to the fact that a bicategory of relations is a -compact (-enriched) category.
Nice, thank you!
Thanks for the feedback! I added some more, related to the Beck-Chevalley condition, with some brief mention there of hyperdoctrines and monoidal fibrations, with a reference to the Brady-Trimble paper mentioned a little while back in connection with strings for monoidal fibrations. Also made a little start on the relation to unitary pretabular allegories.
All this reminds me of the fact that we might put our heads together in various ways. First, string diagrams for monoidal fibrations? Also, I need to get back to some cleanup work on cartesian bicategory, and (no pressure here!) I’d like to see someone write up stuff on equipments and their relations to virtual double categories – I haven’t seen much in the Lab; did I just miss it? I don’t know whether anyone has seriously combined cartesian bicategories with virtual double categories, but it seems an obvious thing to do. (That is, rewrite the definition of cartesian bicategory to take into full account that the vertical arrows of a suitable double category should be maps.)
If I could ask a dim question, in which areas of mathematics would we expect to find cartesian bicategories and bicategories of relations? Is there a wide range of examples?
It’s hard for me to say how wide. The main examples I know of are of type , , and , and so a lot that is in the territory of Lawvere’s notion of generalized logic (as in his early papers on hyperdoctrines) would fit here. It’s closely connected with the groupoidification program (spans of groupoids), although I really ought to check whether the composition by homotopy pullback actually gives a cartesian bicategory. (The composition by strict pullback certainly does.)
Freyd’s own involvement in the allegories approach to relational calculus might have been heavily influenced by his research on the construction of realizability toposes, where one starts with a bicategory of relations (or unitary pretabular allegory = bicategory of relations) of -valued sets, for a set of truth values based on Kleene realizability, and then splits coreflectives = partial equality predicates. The result is another bicategory of relations for a regular category that is a realizability topos. (See Categories, Allegories, 2.153, 2.167, and appendix B, B.312-314.) This is connected with tripos theory as well.
The advantage of Carboni-Walters’ approach to relational calculus is that unlike allegories, cartesian bicategories are not required to be locally posetal, and so they encompass serious bicategorical examples like and . Dropping the local posetal assumption but retaining the (categorified) Frobenius equations, one gets cartesian bicategories whose 2-category of maps is “locally groupoidal” – these include and bimodules between groupoids. (The strong separability axiom imposes a locally posetal character.)
For this reason I think bicategories of relations are in some ways “better” than allegories – the signature is more flexibly adapted to categorification.
But I’m not sure if this is really answering your question.
I don’t know whether anyone has seriously combined cartesian bicategories with virtual double categories, but it seems an obvious thing to do. (That is, rewrite the definition of cartesian bicategory to take into full account that the vertical arrows of a suitable double category should be maps.)
I believe something of this sort, using the language of equipments instead of that of double categories / framed bicategories, is done in the paper “A 2-categorical approach to change of base and geometric morphisms. I” online here. I forget exactly what definition of “equipment” they use (some authors have modified it a bit), but the original notion of equipment (the one described here) is basically equivalent to that of framed bicategory / fibrant double category.
I’d like to see someone write up stuff on equipments and their relations to virtual double categories
Do you really mean virtual double categories, in which the horizontal arrows can’t always be composed? The nlab page on equipments includes the ordinary-double-category point of view. The corresponding notion of virtual equipment is more general and isn’t yet defined on the nLab (it’s been on my to-do list for a while).
In response to David, If I may play devil’s advocate for a moment, I’m not really convinced that any of cartesian bicategories, allegories, etc. are really a natural thing to study in their own right. In most cases it seems to me that the more basic structure is a (cartesian) monoidal fibration or hyperdoctrine or hyperstructure. We can then construct a bicategory from this data, and bicategorical notions in the resulting bicategory may be useful – but I don’t really understand the purpose of axiomatizing the bicategories which arise in this way, instead of axiomatizing the more basic structure. This is also borne out by the fact that considering them as bicategories doesn’t give you the right notion of transformation between them (although that at least is remedied by considering them as double categories instead).
Thanks Todd and Mike for your comments. Something behind what I was asking is a question I have as to the gap between category theory and the mainstream. Some category theoretic constructions, such as adjunction, clearly seem to belong to the Tao of maths (to use a Baezian phrase) and are seen to appear time and again in specific branches of maths. But such appearances are not a necessary condition, since the branches may not have advanced to allow category theoretic construal, or they may have advanced but their exponents may not have noticed the construal. When this is possible, ideally one would be pointed to make moves which might otherwise not have been noticed. Is there an untapped potential out there, so that if only mathematical branch A could be made to think about category theoretic construct B, it could profit? Sometimes it appears that there isn’t as much effort made as there ought to be to make the connections.
@Mike: argh, this is embarrassing. Where you see “virtual double category” in what I wrote in #6, I meant “framed bicategory”. I have no idea how to account for such a mangling of language.
With regard to devil’s advocacy (and putting aside whether one should be considering framed bicategories instead of bicategories), I guess I don’t see why the calculus of relations in a regular category would be most naturally construed in terms of hyperdoctrines.
Edit: Ah yes, I had forgotten about hyperstructures. These I think one could make a serious argument for, inasmuch as imposing a directionality on relations often does feel artificial. In some sense these were anticipated by Peirce as well (who pictured grammatical relations in terms of chemical metaphors, where relations could bond in various directions).
@David: your #10 reminds me of some half-baked thoughts I had during the Langlands Program discussion here.
The Wikipedia entry for motive has
The transition to motives is made by taking the pseudo-abelian envelope of Corr(k):
and links to Karoubi envelope. But is it possible that something about Cauchy completion could be news to people working on motives?
I have no idea how to account for such a mangling of language.
I have one idea – since framed bicategories are actually double categories, it’s natural to want to call them ____ double categories for some value of ____. Sometimes I use ____ = “fibrant”. I sometimes regret ever going along with the name “framed bicategories,” but I don’t really have a better one either.
I guess I don’t see why the calculus of relations in a regular category would be most naturally construed in terms of hyperdoctrines
Perhaps I was using hyperdoctrine wrongly — I just meant a cartesian monoidal fibration in posets with direct images, which relations (or, more precisely, subobjects) in a regular category certainly are. The bicategory of relations is then constructed from that monoidal fibration in the usual way. I guess sometimes (always?) “hyperdoctrine” also means cartesian closure in the fibers, which of course isn’t true in a regular category.
The main difference between such a monoidal fibration and a hyperstructure, as I see it, is that in the former case all the objects are “self-dual”, whereas in the latter the “boundaries” are oriented. So for instance relations and spans fit into the former framework, whereas profunctors requre the latter.
@Mike: I thought you were using the word “hyperdoctrine” correctly – the idea of hyperdoctrine anyway has multiple manifestations, and one of them fits. I just didn’t understand why that would be considered a more natural approach to relational calculus than cartesian bicategories. (Cartesian bicategories feel more natural than allegories to me. The stylistic difference is quite marked: allegories have very lattice-theoretic resonances, and CBs feel like Australian category theory, in other words almost like home to me.)
Something isn’t connecting, then, because the main reason I think of hyperdoctrines as more natural is the same as the reason you gave for why one could make a case for hyperstructures: it’s unnatural to consider only binary relations equipped with a “direction,” instead of n-ary relations for all n. Of course, unlike a hyperstructure, a hyperdoctrine remembers that an n-ary relation on is the same as a unary relation on and encodes it as such. I guess you could say that a cartesian bicategory remembers that as well, and just encodes things in a different way, but it feels more natural to me to encode n-ary relations as unary ones than as binary ones, since doing it that way doesn’t require an arbitrary partition of n into two pieces.
(Do you know what exactly are the origins of “hyper” in “hyperdoctrine” and “hyperstructure”? And whether they’re related?)
but it feels more natural to me to encode n-ary relations as unary ones than as binary ones, since doing it that way doesn’t require an arbitrary partition of n into two pieces.
Well, okay, I see where you’re coming from at least. Just to argue back a little: the fact that functions can be treated on the same level as relations and characterized as left adjoints is IMO a very nice insight, whereas in the hyperdoctrine setting, the morphisms in the base are placed on a separate footing. (This separateness may be related to bicategories vs. framed bicategories.)
Another argument is that the calculus of modules deserves to be considered as having close structural similarities to the calculus of relations, as manifested by the fact that in each case we get a cartesian bicategory. But modules really do have built-in directionality. In some sense ordinary relations and spans are special by the fact that each object is dual to itself, and that accounts for the fact that the calculus of ordinary relations and spans can be re-encoded as a hyperstructure, but not so for the calculus of modules.
(No, I don’t know the etymology of “hyper” in these cases.)
Interesting. Your two arguments seem to me to push in opposite directions, because in the categorified case of modules, it is no longer the case that functors can be characterized exactly as left adjoint modules. So I tend to regard it as an accident of the lower-categorical case that functions can be characterized as left-adjoint relations, because is so happens that every set (and also every poset and every groupoid) is Cauchy-complete. Hence I’m not particularly inclined to prefer a framework which elevates this accident to a fundamental principle, because I’m also interested in the categorified case.
On the other hand, I don’t entirely agree that profunctors have built-in directionality. What they do have is what I might call, in the hyperstructure language, oriented boundaries — in other words, as you say, objects are no longer self-dual. But I don’t see any obstacle to describing this in a hyperstructure-like language, akin to say modular operads. Shoehorning it into a bicategory forces us to distinguish between a profunctor , a profunctor , and a profunctor , which are really the same thing — a hyperstructure would call them all the same.
Moreover, enriched profunctors are no longer a cartesian bicategory (although they are still compact-closed). Thus, it seems very “un-Australian,” to say the least, to focus on cartesian-bicategory language as a way to describe unenriched profunctors.
“Australian” in the sense of taking advantage of 2-categorical algebraic structures – I brought up Australia in the context of cartesian bicategories vs. allegories, and which of the two feels more natural to me. If you’d like to argue for allegories, then I’d be interested, but I don’t think allegories have much to say about enriched profunctors. (Moreover, enriched category theory may not be the first thing that comes to mind in speaking of “Australian category theory”, even if it’s one thing they importantly developed. Perhaps it’s a nebulous phrase to begin with, but 2-dimensional categorical algebra among other things comes to mind, and anyway that’s what I meant.)
Unless you think discussing the meaning of “Australian category theory” would be productive, let’s put that aside for now. I do however welcome your bringing up enriched profunctors; I’ll get back to that in a minute.
I do see, in fact have seen all along, the virtue of treating functions and relations (or functors and modules) separately; the fact that cartesian bicategories of modules detect Morita equivalence but not actual equivalence counts as a strike against it, and there is definitely a point to using some other technology like framed cartesian bicategories or monoidal fibrations to fully address this point. If one chooses one of the latter approaches, then one can always form an underlying cartesian bicategory, where one can assign a predicate to each morphism in the base by quantifying an equality predicate along that morphism, which would then be a map (= left adjoint) in the underlying cartesian bicategory. Since this move is always available, I don’t think the “functions are special relations” point I was making is all that decisive. I’ll go ahead and concede that.
As I understand it, a framed cartesian bicategory approach is more or less equivalent to a monoidal fibration approach (with cartesian base); translating from a framed cartesian bicategory to an associated monoidal fibration is something like a move to focus exclusively on horizontal 1-cells of the form and take those as the generalized predicates, so that pulling back along a morphism in the base is given by precomposing with the associated map to get a 1-cell .I think of the differences are mostly stylistic.
I do think a hyperstructural approach is very interesting, but most people are less used to that than they are to traditional categorical approaches in which composition is performed in a definite direction, and for which there is a large pre-existing literature. So probably which is preferred is a matter of taste. I don’t think that I care too terribly much if some people think a traditional directional approach is “shoehorning” – personally I think that’s a bit overstated. Let’s just say that I think you’ve advanced some good reasons for developing a hyperstructural approach as well (and let individuals decide for themselves which they think is more natural).
I do see your point about oriented hyperstructures being capable of representing module calculus (and funny, I’d thought about modeling free discrete cartesian bicategories in terms of oriented surface diagrams and even did a fair amount of that with Geraldine Brady, but it seems I’d forgotten about that as well), and this would be a fruitful direction for future thinking.
In summary, I think ultimately we share some desiderata. Don’t think I am wedded or hidebound to the idea of sticking to cartesian bicategories or even framed cartesian bicategories. I think they’re pretty neat (and “better” – more flexible than – allegories), but I think we agree that generalized relational algebra ought to be able to embrace the calculus of enriched profunctors as well, and cartesian bicategories don’t handle this case. So I don’t think we are debating or disagreeing as much as may appear to people watching this discussion – mainly I wanted to draw you out on what you meant back in #9 when you said that cartesian bicategories or allegories are less natural than some other things you had in mind. I think I see what you are saying now.
And if you think you’ve worked out the precise structures in which to consider such generalized relational calculus, I’d love to hear about it!
As I said, I was playing a bit of devil’s advocate; I pretty much agree with everything you said in #18. You won’t find me arguing for allegories; I’ve always thought the modular law was one of the most arbitrary axioms I’d ever seen in category theory. But I do wish we had a satisfactory definition of (oriented) hyperstructure.
I thought I’d resurrect this thread because I’ve come across cartesian bicategories and monoidal fibrations in the context of realizability toposes, and I wondered if anyone knew whether the correspondence has been written down anywhere. I’d guess that to get a cartesian bicategory out of a monoidal fibration (following the construction in Mike’s paper) the latter’s total category needs to be cartesian monoidal (Pavlovic calls these regular fibrations). That should include triposes.
I already know that the category of pers in a tripos is the same as the splitting of symmetric idempotents in the corresponding bicategory of relations/allegory (whose category of maps is then a topos). If you split just the coreflexives (in the bicategory corresponding to the effective tripos) you get Freyd et al.’s category of assemblies. The latter is also the regular completion of the category of ’recursively-indexed (nonempty) sets’ used by Robinson and Rosolini to define the effective topos. So it seems that cartesian bicategories are the right context in which to study realizability constructions.
My questions are: is it known whether cartesian bicategories (satisfying some property) are equivalent to regular fibrations (i.e. to monoidal bifibrations with cartesian base and total categories, satisfying Beck–Chevalley and Frobenius)? Has anyone studied the various constructions of the effective topos in this context? I’ve looked at Categories, Allegories, but they don’t seem to mention triposes.
If you can think of a better place to ask this question, please do suggest one. I’m asking here before asking the categories list just in case there’s an obvious answer or a silly mistake that I’ve missed.
Good question! I don’t know enough about cartesian bicategories to answer it; I don’t think I’ve seen an answer given anywhere either. I think you certainly need some property on your cartesian bicategory, since Prof(Set) is a cartesian bicategory (right?) but doesn’t arise from any fibration. In particular, you need something ensuring that every object is its own dual. If you had that, then the data would be determined by the hom-categories with some extra structure, so we could hope to take them as the fiber categories of a monoidal fibration, the base being the category of maps. I was just thinking about something like this the other day, actually; possibly with a bit more work you could actually characterize all bicategories arising from monoidal fibrations, not just the cartesian ones.
Thanks for the feedback, Mike. The property I had in mind (though it’s only a guess at this stage) was the ’maps are comonadic’ axiom in Lack et al.’s paper on bicategories of spans, which implies the Frobenius and Separable axioms they consider: they are enough to make sure that the bicategory of maps is locally essentially discrete. From skimming Carboni–Walters’s proof of compact closedness in Cartesian bicategories I it looks like the discreteness/Frobenius axiom is what makes the nice self-duality business happen.
The paper by Carboni–Kelly–Verity–Wood (whose prequel you cited above) has a remark about (what one might call) cartesian equipments. They might make a good staging-post here.
I’ll see what the list has to say about the realizability applications. With any luck, some of this stuff will make it into my thesis…
1 to 22 of 22