Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: Profunctor composition

Nathaniel Virgo (Mar 26 2020 at 10:20):

I'd like to understand how profunctors compose. (Mostly just for the sake of learning at this stage.) When I read about composition of profunctors I find it's defined in terms of coends, which in turn are defined through a universal property. I'm sure I'll understand that one day, but for now it’s too many abstractions to absorb at once, and I'm wondering if it's possible for someone to describe how profunctor composition works mechanically.

Specifically: I suppose I have a profunctor from C to D (or is it from D to C?) I can think of this as being a category containing all the objects and morphisms from C and D disjointly, together with additional "heteromorphisms" from objects of C to objects of D, which have to compose with the C-morphisms and the D-morphisms. (The definition of a profunctor as a functor from $C^\mathrm{op}\times D \to \mathbf{Set}$ is analogous to the definition of a hom-functor, except that now it maps an object in C and an object in D to the set of heteromorphisms between them.)

If I have two profunctors, say from C to D and D to E, viewed as things that construct categories in this way, then I guess I could just make a new category containing all the morphisms from all three categories and both profunctors, but then I need to have a rule for how the first profunctor’s heteromorphisms compose with the second profunctor’s ones. The obvious choice is just to say that there are no equations - if I have $f:c\to d$ and $f':d\to e$ , then $f;f'$ is just the formal composition $f;f'$ , it's not equal to any other composition of heteromorphisms. Then I could just take all those formal compositions and form a new profunctor from C to E. Is that what the business with coends ends up achieving? Or is it something else?

That’s my guess at horizontal composition, but there is vertical composition as well. My guess is that if you take the above situation and you do start adding equations, then you get a new profunctor from C to E that looks kind of like a subset of the old one. Then vertical composition would be something like an inclusion relation, similar to vertical composition in Rel. Is this guess anywhere near correct?

Matteo Capucci (he/him) (Mar 26 2020 at 10:33):

Profunctor (horizontal) composition should be the usual composition of relations, one level up in the catification hierarchy.
That is, if you have a relation $R \subseteq X \times Y$ and a relation $S \subseteq Y \times Z$ , you get a relation $R;S \subseteq X \times Z$ by defining
$x R;S z \quad \text{iff} \quad \exists y \in Y (x R y \land y S z)$

Matteo Capucci (he/him) (Mar 26 2020 at 10:40):

Now $\exists$ are akin to coends, $\land$ is akin to the monoidal product of the enriching category (e.g. $\times$ in $\bf{Set}$ ) and obviously profunctors are akin to relations. Voilà: let $F: \bf{C} \times \bf{D^{\rm{op}}} \to \bf{Set}$ and $G: \bf{D} \times \bf{E}^{\rm{op}} \to \bf{Set}$ , then you get $F;G : \bf{C} \times \bf{E}^{\rm{op}} \to \bf{Set}$ by defining
$F;G(c,e) = \int^{d:\bf{D}} F(c,d) \times G(d,e)$

Matteo Capucci (he/him) (Mar 26 2020 at 10:42):

(I switched the covariant and contravariant places in the profunctors just to stress the similarity with relations, ofc this is equivalent to the standard convention)

Matteo Capucci (he/him) (Mar 26 2020 at 10:45):

Regarding vertical composition, I'm not aware of this structure. There is an obvious 2-categorical structure on $\bf{Prof}$ given by natural transformations, but those work as usual.

Nicolas Blanco (Mar 26 2020 at 11:07):

In some sense you can also think of a profunctor as a "generalised matrix". To do that you consider a $(m \times n)$ -matrix valued in $\mathbb{K}$ as a function $M : \{1,...,m\} \times \{1,...,n\} \to \mathbb{K}$ . Then profunctor composition is similar to matrix multiplication :
$(N \circ M)(i,k) = \sum_j M(i,j) N(j,k)$

Nicolas Blanco (Mar 26 2020 at 11:08):

I am not sure what you mean by vertical composition.

Jules Hedges (Mar 26 2020 at 11:11):

The previous answers fit together, since relations (between finite sets at least) compose like matrices over the boolean ring

Nathaniel Virgo (Mar 26 2020 at 11:14):

I understood (maybe incorrectly?) that categories and profunctors form a 2-category in the same way that categories and functors form a 2-category. In the latter case, natural transformations are the vertical composition of functors, so there should be something analogous for profunctors. That is, if I have two profunctors from C to D, there should be some notion of morphism between them.

Nathaniel Virgo (Mar 26 2020 at 11:14):

Anyway my question is just whether the definition in terms of coends works out to the same as the mechanical picture I sketched.

Nathaniel Virgo (Mar 26 2020 at 11:16):

(My situation is analogous to that of someone who sort of vaguely understands the definition of a categorial product, and who has guessed that the product in Set might be given by the Cartesian product, but who isn't sure and needs a bit of a hint.)

Nicolas Blanco (Mar 26 2020 at 11:18):

Oh okay. In fact categories and profunctors form a bicategory (aka weak 2-category) since composition of profunctors is associative only up to isomorphism. Vertical composition of profunctors is also given by natural transformations.

Nathaniel Virgo (Mar 26 2020 at 13:28):

Thanks, that's useful information.

I'm not sure if this makes any sense to anyone but me, but here's what a natural transformation looks like in the mental picture I'm trying to draw. I'm thinking of a profunctor as something like this. It's a category containing C and D as subcategories, together with morphisms from objects c, c' of C to objects d, d' of D. (There are also morphisms from c' to d and c to d', but I haven't drawn them.) image.png

To avoid clutter, let's draw the het-sets like this:
image.png The red arrow is a function which just represents the composition rule, $h \mapsto j;h;k.$

Then a natural transformation between two profunctors is just another set of functions, such that the red and blue arrows form a commuting square below.
image.png

Probably this is all just obvious to someone with more experience, but I find these kinds of pictures help me to get a better feel for the concepts, at least while they're still new.

So that covers vertical composition - great! - can we draw something similar for horizontal composition? (I think so, and I think I have a good idea what it is - the only stumbling block is not being sure about what the coend integral notation does in this picture.)

Nathaniel Virgo (Mar 26 2020 at 13:37):

(with many thanks to my wife for letting me borrow her iPad and stylus. It was pretty intuitive and painless to draw and share those diagrams - maybe a nice tip for anyone who has access to one.)

Nathanael Arkor (Mar 26 2020 at 13:40):

@Nathaniel Virgo: I think a good intuition for the coend notation is existential quantification
so if you take profunctors $F : D^\circ \times C \to \mathbf{Set}$ and $G : E^\circ \times D \to \mathbf{Set}$ , their composite is defined as $(G \circ F)(e, c) = \int^{d \in \mathscr D} F(d, c) \times G(e, d)$ , which you can read as $\exists d \in \mathscr D . c \to d \land d \to e$

Nathanael Arkor (Mar 26 2020 at 13:40):

and it's clear from the existential formulation that this corresponds to something that looks like composition

Nathanael Arkor (Mar 26 2020 at 13:41):

(the arrows are reversed compared to how they appear in the coend because of the variance)

Nathanael Arkor (Mar 26 2020 at 13:42):

(I see this is essentially what @Matteo Capucci says, scrolling back — I'm just using $\to$ instead of $R$ )

Thomas Read (Mar 26 2020 at 14:05):

If I have two profunctors, say from C to D and D to E, viewed as things that construct categories in this way, then I guess I could just make a new category containing all the morphisms from all three categories and both profunctors, but then I need to have a rule for how the first profunctor’s heteromorphisms compose with the second profunctor’s ones. The obvious choice is just to say that there are no equations - if I have $f:c\to d$ and $f':d\to e$ , then $f;f'$ is just the formal composition $f;f'$ , it's not equal to any other composition of heteromorphisms. Then I could just take all those formal compositions and form a new profunctor from C to E. Is that what the business with coends ends up achieving? Or is it something else?

You'll have equations corresponding to the category structure of $D$ . You want to quotient out the formal compositions by the equivalence relation generated by:
if $f : c \to d$ , $g : d \to e$ , $f' : c \to d'$ , $g' : d' \to e$ are "heteromorphisms", and $\varphi : d \to d'$ is a morphism in $D$ such that $f ; d = f'$ and $g = \varphi ; g'$ , then you equate the formal compositions $f ; g$ and $f' ; g'$ .

Nathaniel Virgo (Mar 26 2020 at 14:48):

Nathanael Arkor said:

Nathaniel Virgo: I think a good intuition for the coend notation is existential quantification
so if you take profunctors $F : D^\circ \times C \to \mathbf{Set}$ and $G : E^\circ \times D \to \mathbf{Set}$ , their composite is defined as $(G \circ F)(e, c) = \int^{d \in \mathscr D} F(d, c) \times G(e, d)$ , which you can read as $\exists d \in \mathscr D . c \to d \land d \to e$

This is useful but seems not to tell the whole story - $\exists d \in \mathscr D . c \to d \land d \to e$ tells me whether there exists a heteromorphism from $d$ to $e$ or not, but to go from relations to categories this should change from a Boolean value to a set. The place I'm stuck is in the details of how to make that transition.

Nathaniel Virgo (Mar 26 2020 at 14:51):

Thomas Read said:

You'll have equations corresponding to the category structure of $D$ . You want to quotient out the formal compositions by the equivalence relation generated by:
if $f : c \to d$ , $g : d \to e$ , $f' : c \to d'$ , $g' : d' \to e$ are "heteromorphisms", and $\varphi : d \to d'$ is a morphism in $D$ such that $f ; d = f'$ and $g = \varphi ; g'$ , then you equate the formal compositions $f ; g$ and $f' ; g'$ .

This is the kind of mechanical explanation I was hoping for! Does $\varphi$ have to be an isomorphism or is it really for any morphism? I will have to think a bit about why things have to be defined this way. (Any insight appreciated.)

Nathanael Arkor (Mar 26 2020 at 14:59):

to go from relations to categories this should change from a Boolean value to a set

instead of thinking of $\exists$ as true or false, you can think of it as quantifying all those elements for which it is true

Thomas Read (Mar 26 2020 at 15:04):

Nathaniel Virgo said:

This is the kind of mechanical explanation I was hoping for! Does $\varphi$ have to be an isomorphism or is it really for any morphism? I will have to think a bit about why things have to be defined this way. (Any insight appreciated.)

Any morphism

Thomas Read (Mar 26 2020 at 15:14):

I imagine someone else can tell us about properties of the bicategory of profunctors that make it really convincing that this is the right definition.

Intuitively I guess you want to use all the data from $D$ , not just the objects or even just the isomorphisms.

One point is that hom functors $C^\text{op} \times C \to \text{Set}$ are identities with respect to horizontal composition - if you defined horizontal composition differently you probably wouldn't be able to find an identity.

Nicolas Blanco (Mar 26 2020 at 15:57):

If you think of a profunctor as a functor $F : C \to Psh(D)$ - essentially by currying - then composition is given by composing with the left Kan extension along the Yoneda embedding $G \circ F = Lan_y(G) \circ F$ :
temp.pdf
And the identity is the Yonead embedding.
Said like that it might seem obscure but when you look at the diagram it make a lot of sense.
You have two functors $F : C \to Psh(D)$ and $G : D \to Psh(E)$ and you want to get a functor $C \to Psh(E)$ .
To do that you need a to get a functor $Psh(D) \to Psh(E)$ from $G$ . The "obvious" choice is the left Kan extension along the Yoneda lemma.

Mike Stay (Mar 26 2020 at 15:59):

(Any insight appreciated.)

The elements of an adjacency matrix for a graph count the paths from one vertex to another. The elements of a profunctor are the sets of heteromorphisms from one object to another rather than just the number of them. To compose the adjacency matrices of two bipartite graphs, you multiply their adjacency matrices. To compose two profunctors, you do matrix multiplication, but where multiplication is all pairwise compositions and addition is union.

Nathaniel Virgo (Mar 26 2020 at 16:52):

Great, this is pretty perfect. When we combine Mike Stay's argument above with Thomas Read's point about hom-functors being the identity, we get the complete picture. (Modulo me actually understanding coends properly and seeing why they yield this construction, but that's a task for later.)

The important point is that addition is union, but not disjoint union - some paths are considered equal to others. If we want to have this
(image drawn in Keynote because the iPad needs charging)

then it pretty much forces us to say that whenever we have a set of paths like this that commute
...

then we have to consider them equal to each other.

Thomas Read (Mar 26 2020 at 17:10):

:grinning: those diagrams are great

T Murrills (Mar 27 2020 at 00:54):

I don't understand things here fully yet, but answering this question might help me: why do we use coends and not ends?

Also, is there an analogous notion of composition (or even a whole separate analogous definition of profunctors—coprofunctors? procofunctors?) that uses ends for composition instead? (I'm guessing there's also a chance products become coproducts to make things work out?) (Obviously we could just dualize everything in sight, but I'm wondering if there's a nontrivial version that just uses some of the dual concepts.)

This is suggested by the fact that we can define composition for relations in a couple different (nonstandard) ways.

(More generally, I wonder what characterizes the compositions that are categorifiable, if not all; and if there's a generic prescription for categorification of these definitions, about which we might hope to prove that it produces some sort of "coherence", instead of just being a heuristic analogy that we check works out in each case.)

tangent: one reason for me to be a little doubtful from the outset, though (before knowing what I'm doing—I'm just spitballing at this point) is that if the use coends is tied to the use of products, then there are a couple product structures "baked in" to the notion of a category that might determine it. For one, composition of ordinary arrows is a mapping from the product of hom's, and (more directly relevant here) hom is a bifunctor from the product of a category with its op, from which we analogize to conceptualize profunctors as yielding "heteromorphisms" as above. So, potentially, if it does lead down that rabbit hole...who's up for defining "cocategories" that either 1) involve a "cocomposition" (equivalently, "mposition", of course) that somehow use coproducts of homs instead of products, and/or 2) have a structure somehow given by a "cohom" functor involving the coproduct of a category with its op? :)

Nathanael Arkor (Mar 27 2020 at 01:00):

ends are like universal quantification, rather than existential quantification

This is suggested by the fact that we can define composition for relations in a couple different (nonstandard) ways.

can you suggest a definition of relational composition that uses universal quantification?

Nathanael Arkor (Mar 27 2020 at 01:02):

that if the use coends is tied to the use of products

if the product you're referring to is the one in the composition coend formula, this corresponds to the tensor product in the enriching category

Nathanael Arkor (Mar 27 2020 at 01:03):

also, cocategories are a thing: https://ncatlab.org/nlab/show/cocategory :)

Nathanael Arkor (Mar 27 2020 at 01:10):

More generally, I wonder what characterizes the compositions that are categorifiable, if not all

I think the general opinion (here at least) is that we would like most concepts to be categorifiable :)

Nathanael Arkor (Mar 27 2020 at 01:10):

but there isn't a general technique for doing it in most cases

Nathanael Arkor (Mar 27 2020 at 01:11):

there are some results along those lines, say for "linear algebraic theories" (https://arxiv.org/abs/1002.0879)

T Murrills (Mar 27 2020 at 02:26):

so, for instance, I could try just replacing existential quantification: $c(R \circ S)b \iff \forall d: cRd \wedge dSb$ .

Okay, I'm seeing now that that doesn't have identities! Swapping out the and for an or, or replacing the connective, say with an if or an iff, seems at first glance to produce similar problems.

This makes me suspect that the standard composition for Rel is actually quite special, and might be determined in some way by the very demand that we produce a "categorical" composition (associative, identities) on relations. Is that the case, somehow? Is the standard composition the only such elementary composition we could have on relations?

if the product you're referring to is the one in the composition coend formula, this corresponds to the tensor product in the enriching category

so, are coends specially tied to the tensor bifunctor in a way that ends aren't? (I know the bare definition for coends, but have no intuition on how they work, or—in particular—why a coend actually works here and an end doesn't, besides vague analogy. Maybe I just need to draw out the arrows and find out that they face similar problems as the decategorified case!)

Christian Williams (Mar 27 2020 at 06:01):

I really support the feeling that the dualities of category theory should always be "completed" somehow. It seems like such a deep topic. Even though category theory has "duality baked in", what at first glance seems like just a $\mathbb{Z}_2$ -action on $\mathrm{Cat}$ becomes a many-dimensional and many-layered notion...

Christian Williams (Mar 27 2020 at 06:02):

One can say that "a category is a monad in the bicategory of spans", and then "op" arises from the fact that $\mathrm{Span}$ is compact closed; it has a duality involution given by swapping span legs. The "monad in spans" approach leads to the definition of cocategory, which is "a comonad in cospans". Then rather than "composing by pullback" you "cocompose by pushout". There are people that think about these things, and even a good exposition: http://www.math.jhu.edu/~tclingm1/store/cocategories.pdf.

Christian Williams (Mar 27 2020 at 06:07):

When it comes to a very "high-level swap" (to me) like ends and coends here, it's almost enough to make you dizzy. The analogy with relations and quantification definitely brings it down to earth, so you can at least think about swapping $\exists$ for $\forall$ . But like you said, that doesn't seem to give an operation with a hope of being associative or unital. Any way, I'm sure there's some flexibility here to make alternative notions of composition.

Christian Williams (Mar 27 2020 at 06:12):

One thing that's always been mysterious to me is the fact that you can think of profunctors both as generalized bimodules and as generalized linear maps.

Christian Williams (Mar 27 2020 at 06:12):

There is a general notion of a "module of a monad", and in this "categories as monads" perspective, profunctors are exactly bimodules - and profunctor composition is "bimodule tensor" (coequalizing by the left/right actions of the middle category).

But as y'all have been saying, you can also think of profunctors as matrices - and composition is "matrix multiplication" (with some quotienting, as discussed).

Christian Williams (Mar 27 2020 at 06:12):

These seem like opposing interpretations! How is this concept both a "vector space" and a "linear map" at the same time?

sarahzrf (Mar 27 2020 at 07:38):

oo i missed this topic :eyes:

sarahzrf (Mar 27 2020 at 07:44):

@Nathaniel Virgo honestly Set-valued coends seem to in general have a strong flavor of "making formal compositions associative", based on my limited experience

sarahzrf (Mar 27 2020 at 07:44):

another really good example of a coend to chew on is day convolution, which lets you put a monoidal structure on the category of presheaves on a monoidal category

sarahzrf (Mar 27 2020 at 07:46):

basically: say $C$ is a monoidal category. say we want to be able to take the tensor product of presheaves on $C$ , and we want it to agree with the existing one when the presheaves are representable. so: say we have presheaves $F, G$ —to define what $F \otimes G$ should be, we need to ask, what do morphisms $A \to F \otimes G$ look like for representable $A$ ?

sarahzrf (Mar 27 2020 at 07:49):

well: we can say that they factorize as 2 steps:

go $A$ to $B_1 \otimes B_2$ for representable $B_1, B_2$ , so that we're still working within $C$ and we can account for this with our existing tensor product.
go $B_1 \otimes B_2 \to F \otimes G$ by taking the tensor product of some $B_1 \to F$ and $B_2 \to G$ , which we already understand.

sarahzrf (Mar 27 2020 at 07:53):

so we can define $(F \otimes G)(A)$ for $A \in C$ as the set of formal compositions $A \to B_1 \otimes B_2$ followed by $y(B_1), y(B_2) \rightrightarrows F, G$ —except this isn't quite right, we need to quotient a bit

sarahzrf (Mar 27 2020 at 07:53):

and that's exactly a coend

sarahzrf (Mar 27 2020 at 07:54):

$\int^{B_1, B_2} C(A, B_1 \otimes B_2) \times F(B_1) \times G(B_2)$

sarahzrf (Mar 27 2020 at 07:54):

(where the yoneda lemma has been used to minify a bit)

sarahzrf (Mar 27 2020 at 08:19):

(this can alternatively be given as a profunctor composition or a kan extension, actually)

sarahzrf (Mar 27 2020 at 08:21):

fun exercise: show that if $C$ is a discrete category, so that $\otimes$ just forms a monoid, then if presheaves $F, G$ take only subsingleton values, meaning that they can be identified with subsets of $C$ , then $F \otimes G$ in fact corresponds to $\{x \otimes y \mid x \in F,\ y \in G\}$

Nicolas Blanco (Mar 27 2020 at 09:51):

Christian Williams said:

These seem like opposing interpretations! How is this concept both a "vector space" and a "linear map" at the same time?

Bimodules can be understand as generalised maps. For example any ring homomorphism $f : R \to S$ gives raise to a $(R,S)$ -bimodule on $S$ with left action multiplication by the image of $f$ and right action multiplication. This can be generalised to bimodule over a monoid (internal to some category) and then to enriched bimodules a.k.a. enriched profunctors by considering a monoid internal to $\mathcal{V}$ as a $\mathcal{V}$ -enriched category with one-object. In this setting it just states that any enriched functor $F : \mathcal{C} \to \mathcal{D}$ gives a profunctor $Hom_{\mathcal{D}}(-,F(-)) : \mathcal{D}^{op} \times \mathcal{C} \to \mathcal{V}$ .
This is just to say that it is often better to think of bimodules as morphisms and not as objects.
I am not sure really familiar with "module of a monad" so I am not sure how it fits in this picture.

Robin Piedeleu (Mar 27 2020 at 12:35):

T Murrills said:

so, for instance, I could try just replacing existential quantification: $c(R \circ S)b \iff \forall d: cRd \wedge dSb$ .

Okay, I'm seeing now that that doesn't have identities! Swapping out the and for an or, or replacing the connective, say with an if or an iff, seems at first glance to produce similar problems.

This makes me suspect that the standard composition for Rel is actually quite special, and might be determined in some way by the very demand that we produce a "categorical" composition (associative, identities) on relations. Is that the case, somehow? Is the standard composition the only such elementary composition we could have on relations?

To define another structure of category on relations, you can modify the composition you have given to use a disjunction instead of a conjunction. This is an associative operation and it is unital with identities $\{(x,y) | x\neq y\}$ ). But this category is equivalent to the category of sets and relations with the usual composition (using existential quantifiers and conjunction). In fact, the equivalence is just negation, mapping a relation to its complement!

This also extends to a monoidal equivalence, taking the Cartesian product of sets as monoidal product for objects in both categories but using conjunction in one case and disjunction in the other, for morphisms.

Max New (Mar 27 2020 at 15:42):

Some have talked about how profunctors form a 2-category, or really a bicategory. I think the most natural categorical structure to describe them is a double category, which includes the strucure of functors and profunctors and the relationship between them is described by the structure of a proarrow equipment. I think the UCR seminar next week will go over double categories if you are interested to learn more.

sarahzrf (Mar 27 2020 at 15:43):

ive been meaning to learn about double categories! ive heard they're cubical when ordinary bicategories are globular, or something to that effect

Max New (Mar 27 2020 at 15:56):

Yes something like that. The 2-cells are squares where the top and bottom squares come from the class of "horizontal" arrows and the left and right sides come from the "vertical" arrows. The nlab has a nice diagram. I find it makes the diagrams easier to draw :)

Nathaniel Virgo (Mar 27 2020 at 17:48):

I'm way out of my depth at this point (which is fine, I'll catch up once I've levelled up enough), but I wonder if this double category thing has to do with something I noticed way up above after I drew this:
image.png

I drew the blue arrows to represent a natural transformation between the two profunctors, but in this profunctors-as-categories picture they can also be seen as a functor mapping the 'F' category to the 'G' category. If vertical morphisms between profunctors can be seen as functors then you can consider natural transformations between those functors, which adds another level to the category. I've no idea what that means practically, I just thought it was neat.

Mike Stay (Mar 27 2020 at 19:06):

@Nathaniel Virgo I haven't seen any treatment of this, but it seems like you ought to be able to define a bicategory Prof(C, D) of profunctors, natural transformations, and modifications. Letting your two blue arrows be $\alpha, \beta\colon F \Rightarrow G$ , note that as functors between the collages $F, G$ they preserve objects on the nose. A modification $\Gamma\colon \alpha \Rrightarrow \beta$ would be:

a natural transformation $\Gamma_C$ on the identity functor on C
a natural transformation $\Gamma_D$ on the identity functor on D

such that for all heteromorphisms f in F(c, d), the following square commutes:

     α_(c,d)(f)
c ----------------> d
|                   |
| Γ_c               | Γ_d
|                   |
V                   V
c ----------------> d
     β_(c,d)(f)

Mike Stay (Mar 27 2020 at 19:13):

The nearest thing I can think of is Hoffnung's paper https://arxiv.org/abs/1112.0560, leaning on the similarity between spans of categories and profunctors.

John Baez (Mar 27 2020 at 20:39):

By the way, it's worth noting that starting with any category with pullbacks you get an infinity-category of objects, spans, spans of spans, spans of spans of spans, ... just like that Viking song in Monty Python.

Mike Stay (Mar 27 2020 at 21:16):

@John Baez But I'd expect Prof to be more similar to spans, maps of spans, and maps of maps of spans, where at some point the only things "between" two n-morphisms are equalities.

John Baez (Mar 27 2020 at 22:35):

I guess maybe. But there could be a version that goes on forever too.

Mike Stay (Mar 28 2020 at 00:16):

Sure. But I'd expect the thing analagous to spans of spans to be something like a "pronatural transformation", something that works out to be a profunctor between the collages.

Beppe Metere (Mar 28 2020 at 14:51):

I'd like to add a complementary point of view.

A leit-motive in introducing profunctors is considering them as a sort of $2$ -dimensional version of the set-theoretical notion of relation. Actually, a relation from $A$ to $B$ can be identified with its characteristic function $A\times B\to 2$ . The dimensional shift then suggests to define a notion where the sets $A$ and $B$ are replaced by categories, and the set $2$ is replaced by the category $\mathbf{Set}$ of sets. Hence, a profunctor from $A$ to $B$ is identified with a functor $A^*\times B\to \mathbf{Set}$ , where $A^*$ is the opposite category of $A$ , which is necessary in order to deal with arrows of categories. Given these definitions, profunctor composition is the $2$ -dimensional version of relation composition, which has been discussed above.

Now, there is (at least) another relevant approach to the notion of profunctor, which I prefer because it is more suitable for dealing with internal structures. Let me explain it, by starting again from the easier case of relations.

The relation $A\times B\to 2$ is in fact better known as a subset of the product $A\times B$ , i.e. a subobject $R\to A\times B$ . Composing with product projections, one gets a span $A \leftarrow R\rightarrow B$ , where the two legs of the span are jointly monic. With this definition, the composition of $R$ with the another relation, say $B \leftarrow S\rightarrow C$ can be obtained by taking the composition of these two spans, and then shrinking the resulting big span. More precisely one takes the pullback $RS$ of the cospan $R\rightarrow RS\leftarrow S$ and compose projections with the other legs in order to get the new span $A\leftarrow R\leftarrow RS\rightarrow S\rightarrow C$ . Unfortunately, this new span is not a relation, because its two legs ar not jointly monic, but this is not a big deal, since it suffices to take the image of the joint legs map $RS\to A\times C$ , which is precisely the composition of relations $R\circ S$ .

Relations in $\mathbf{Set}$ can be considered as 'relative to a factorization system' namely, the image factorization. More precisely, given sets $A$ and $B$ , image factorization gives the local reflections $\mathbf{Span}(A,B)\to\mathbf{Rel}(A,B)$ .

It would be nice if something similar could be done for profunctors, and indeed it is so. The easier case is that of groupoids. Groupoids are categories where all arrows are iso, and a profunctor between groupoids is defined in the same way as for categories (but in the case of groupoids its definition can be simplified). In the category of groupoids there is a very nice factorization system that collapse three different factorization which are possible for functors between categories:

final / discrete fibration
initial / discrete opfibration
full + essentially surjective / faithful

In fact it is possible to prove that profunctors between groupoids are precisely the relations relative to such factorization system. Therefore, one can calculate their composition by taking the pullback of the corresponding spans, and the taking the 'final' image of the resulting big span. All the details can be found in a recent paper of mine:

G. Metere, Distributors and the comprehensive factorization system for internal groupoids, Theory and Applications of Categories, Vol. 34 no. 1 (2019).

...where profunctors are called 'distributors', as they where named by Jean Benabou.

Concerning categories the situation is a bit more involved, since the three factorization systems above remain distinct. In fact it is still possible to compute the composition using a factorization system, but in this case one should interpret a profunctor from $A$ to $B$ as its corresponding $2$ -sided discrete fibration $R\to A\times B$ fibred over $A$ (or op-fibred over $B$ ), and then taking the initial image in $\mathbf{Fib}(B)$ or the final image in $\mathbf{opFib}(A)$ .

Ciao,

Beppe.