Re #18: that’s what I’d say. In some sense such are subsumed under ordinary profunctors $A^{op} \otimes B \to V$ where $A = A_1 \otimes \ldots \otimes A_m$ and $B = B_1 \otimes \ldots \otimes B_n$, although there is a faint suggestion of thinking more in terms of composing along morphisms in just one $A_i$ or $B_j$ at a time, rather than jointly.

]]>Hadn’t read the blog post yet…that’s great, thanks!

]]>Noam, in the post of Robin Houston linked to above, he calls them “relational profunctors”. Not sure how widespread that is. Personally, I’m content to call them 2-enriched profunctors (and like the word “bimodule” even more than “profunctor”).

]]>Re #15

(Also, what happens to ternary and higher-ary relations?),

do we just take the product of the covariant arguments, and also of the contravariant arguments, and then look at profunctors between these products?

]]>Speaking of which, does anyone if there is a name for the “posetal compromise” between Rel and Prof, i.e., the bicategory whose objects are posets $A,B$, morphisms $M : A ⇸ B$ are downwards closed subsets $M \subseteq A^{op} \times B$, and 2-cells $M \Rightarrow N$ are inclusions $M\subseteq N$?

]]>Re #15: it’s based on the fact that a set when seen as a discrete category is equivalent to its opposite. You could say that the low dimension is partly to “blame”, but note that a groupoid $G$ is also equivalent to its opposite, where morphism inversion gives a functorial equivalence $G^{op} \to G$.

]]>A profunctor is contravariant in one argument. So is the symmetry of Rel only a coincidence in low dimension?

(Also, what happens to ternary and higher-ary relations?)

]]>A profunctor.

]]>Prof.

]]>Thanks Todd Trimble for updating the “functional relation” page, this is all very interesting.

By the way, what is the higher equivalent of a relation? (Or, what is the categorification of Rel analogous to Cat for Set?)

]]>One advantage of allegories over regular categories is that quotients of equivalence relations in allegories (and “framed allegories”) can be described as an enriched weighted colimit therein.

]]>From another perspective on the question, SEAR is a development of elementary structural set theory in which binary relations are fundamental and functions are derived.

]]>Right: the statements when suitably internalized hold in any topos and more generally in any regular category.

I don’t think the sniffer was entirely accurate. There’s pretty much a perfect dictionary between regular categories and (unitary) *tabular* allegories (where every arrow is “tabulated” by a span-pair of left adjoints, as in the picture at functional relation). But I do think that allegories cast a slightly different light on things, and can be useful. For example, examples of realizability toposes can be rather neatly described in allegorical terms. Taking a step back, I think it can be useful to consider relations as primary and functions derived, just as it can be useful to consider bimodules as basic in enriched category theory.

Maybe I’d think it more accurate to say that allegories are something of an acquired taste for certain crowds. To a category theorist, the Freyd modular law on which the whole theory hangs may look a little bizarre, and I have to say I’m spiritually in agreement with Bob Walters where he subordinates the modular law to a “more natural-looking” Frobenius condition which is connected with 2d cobordism theory. Thus, the notion of bicategory of relations, which also takes relations as basic, may seem nicer to category theorists. But to someone more inclined to lattice theory, I can imagine the allegory axioms being pregnant with meaning, and the whole development sort of exciting.

]]>I’m not sure it makes sense to talk about $Rel$ “enriched” in another topos, but you can define a bicategory $Rel_T$ of relations *internal to* any topos $T$, and then I believe the adjunctions in $Rel_T$ correspond to morphisms in $T$, just as in the case $T = Set$.

I have not checked this, but I think this basic sort of stuff works just as well in any topos.

Does the same sort of result hold if $T$ is a regular category? When I mentioned allegories to a couple of famous Australian category theorists, many years ago, one of them sniffed that they’d been subsumed by the theory of regular categories.

]]>Are adjunctions in * Rel* internal to a different topos other than

Edit: internal to, not enriched in.

]]>I added to functional relation some narrative and argumentation, and references including Robin’s blog post, but didn’t labbify to the extent of sticking the arguments in proof environments. Most but not all the points in the blog post were touched upon; on the other hand, some arguments which Robin left to the reader are spelled out.

]]>Of course we ought to be considering whether such information is adequately represented on the nLab. We have functional relation. Anything clearer at the blog post of #2 than here?

]]>Yes, that functions are precisely left adjoints in the bicategory of relations is a good exercise. Their right adjoints are their relational opposites.

Try getting a hold of *Categories, Allegories* by Freyd and Scedrov – allegories take relations as primary and give axiom systems for them. Similarly you should get a hold of some of the literature on cartesian bicategories, e.g. Cartesian Bicategories I by Carboni and Walters.

Very nice! Thank you!

]]>See eg this blog post

]]>Consider sets and functions. A relation between two sets can then be expressed as a subset of a Cartesian product, in other words, we can define it and describe it using functions.

Viceversa, can we describe functions using relations as the “fundamental” arrows? That is, can we define and describe functions without using other functions, only relations?

]]>