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: practice: terminology & notation

Topic: What is a profunctor C ⇸ D?

Max New (Nov 07 2022 at 22:50):

I am implementing some of the theory of profunctors in the cubical agda repo and in the discussion on my pull request we are faced with my most dreaded bike-shedding question: does a profunctor C ⇸ D mean a functor $C^o \times D \to \textrm{Set}$ or $D^o \times C \to \textrm{Set}$?

Personally, it seems completely natural to me that it would be the former, as when you have R : C ⇸ D you would then write $R(c,d)$ when applying it to objects, and the order of the variables matches the order you write them in the type of R, simple. However this seems to be the opposite of the convention on the nlab and Benabou, so I would like to at least hear the argument for the other notation.

The argument on the nforum (https://nforum.ncatlab.org/discussion/10145/profunctor/?Focus=96048#Comment_96048) seems to be that people prefer the convention $D^o \times C \to \textrm{Set}$ because then this is the same as $C \to \hat D$, i.e., a functor to the presheaf category on $D$ and since presheaf categories are more common in practice/by convention than their dual that we should pick the orientation that matches that.

Idk this argument just doesn't seem that compelling to me? It seems weird for me to flip something in a definition rather than just flip it in an application? It seems to me that if you showed a student the definition of profunctor for the first time they would not be confused by the $C^o \times D \to \textrm{Set}$ definition and they would be confused by the other. Then I would have to explain that in (of course very important) applications that they might never work on that the other convention is more natural.

I honestly hate that I even made this thread because I hate bike-shedding but I want to give the other side a chance before we commit to a particular choice in the library.

John Baez (Nov 07 2022 at 22:55):

The idea of the nLab, as far as I can tell, is that thanks to the Yoneda embedding $y: D \to \hat{D}$, a functor from $C$ to $D$ can be seen as a special case of a functor from $C$ to $\hat{D}$, so the latter should be called a profunctor $C$ ⇸ $D$.

John Baez (Nov 07 2022 at 22:56):

In other words, while a functor sends objects of $C$ to objects of $D$, which correspond to representable presheaves on $D$, a profunctor sends objects of $C$ to general presheaves on $D$.

John Baez (Nov 07 2022 at 23:02):

I don't see why you think of the nLab's preference as involving an "application" of profunctors. To me it seems based on a way of thinking about how profunctors generalize functors - or in other words, a way of understanding profunctors.

Nathanael Arkor (Nov 07 2022 at 23:04):

The bicategory of profunctors is the Kleisli bicategory for the presheaf construction. This doesn't seem like "flipping something in a definition": one could argue that this is how profunctors ought conceptually to be defined. Furthermore, with this convention the representable profunctor associated to a functor $A \to B$ goes from $A$ to $B$, whereas the corepresentable profunctor goes from $B$ to $A$, which seems much more natural than the opposite.

Max New (Nov 07 2022 at 23:04):

I get that, but on the other hand, if I'm reasoning about an isomorphism of the form Hom[F c, G d] =~ R(c,d) then I'm always flipping the order of the arguments between when I write the type of R and when I apply it to arguments.

John Baez (Nov 07 2022 at 23:06):

Yeah, that's the argument on the other side.

John Baez (Nov 07 2022 at 23:07):

If there weren't arguments on both sides presumably people would all agree.

Max New (Nov 07 2022 at 23:08):

It just doesn't bother me or annoy me at all that $C \to \hat D$ has to be turned into $D$ ⇸ $C$. It's seems to me like complaining that there's an op in the definition of the presheaf category.

Nathanael Arkor (Nov 07 2022 at 23:11):

If you're replying to my message, I think you misunderstand. With your proposed notation, Prof is biequivalent to the opposite of the Kleisli bicategory of the presheaf construction, which I think is really overlooking a fundamental aspect of the nature of profunctors.

Max New (Nov 07 2022 at 23:11):

It's overlooking because it involves an op?

Nathanael Arkor (Nov 07 2022 at 23:12):

Both sides could say that the other side is overlooking an op, because the two perspectives differ only by an op...

John Baez (Nov 07 2022 at 23:14):

With your convention, Max, I'd be saying things like "composing the functor $F: C \to D$ and the profunctor $G: E$ ⇸ $D$ we get a profunctor from $E$ to $C$." I find this confusing - in fact it took me over a minute to work it out.

I'd rather say "composing the functor $F: C \to D$ and the profunctor $G: D$ ⇸ $E$ we get a profunctor from $C$ to $E$." That's how it works with the nLab conventions.

Max New (Nov 07 2022 at 23:14):

It doesn't seem to change anything to me to say that Prof is biequvalent to the Kleisli bicategory or its opposite. It is just as important IMO that it is equivalent to the Kleisli bicategory of the copresheaf construction. What is important is that you have both, and you get that each functor induces an adjoint pair of profunctors

Nathanael Arkor (Nov 07 2022 at 23:19):

I'm not explaining myself very well; let me start over. (I removed my other messages, because I think they were confusing.)

Nathanael Arkor (Nov 07 2022 at 23:26):

One can consider two bicategories: the Kleisli bicategory of the presheaf construction, and the Kleisli bicategory of the copresheaf construction. The first corresponds to what is usually called Prof in the literature (which is the opposite to your notation), whereas the second corresponds to Prof^co. If you flip the convention for 1-cells in Prof, then you must add ^op to both definitions. To me, this appears inelegant, since from a conceptual point of view, one ought to view profunctors as Kleisli 1-cells (as espoused in the paper on relative pseudomonads, for instance). Of course, the only thing that changes if you use the other convention is that you need to add ops, so it is easy to justify it as being a minor concern. However, I would argue that the conceptual advantage outweighs the occasional practical disadvantage.

Nathanael Arkor (Nov 07 2022 at 23:29):

(Furthermore, from a practical perspective, it is easy to either apply profunctors only to pairs to avoid any confusion about application order, or to use (co)representable presheaves to apply profunctors via composition.)

Mike Shulman (Nov 07 2022 at 23:47):

Here's another way of saying it. There are two pseudofunctors from $\rm Cat$ to $\rm Prof$, which are the identity on objects and send each functor to its representable and corepresentable profunctors. If you define a profunctor from $C$ to $D$ to be covariant in $C$ and contravariant in $D$, then these two functors are $\rm Cat \to Prof$ and $\rm Cat^{coop}\to Prof$. If you make the other choice, then they are $\rm Cat^{co} \to Prof$ and $\rm Cat^{op} \to Prof$. Many people find it nicer and more convenient, especially when working abstractly with proarrow equipments from the pseudofunctor perspective, to have one of these functors be "totally covariant".

Max New (Nov 07 2022 at 23:47):

Here's the definition I would use: A profunctor P : C ⇸ D is a functor $C^o \times D \to \textrm{Set}$ and a 2-cell $\phi : P \multimap Q$ is a natural transformation $\phi_{c,d} : P(c, d) \to Q(c, d)$. This is a virtual equipment so there's a unit profunctor $U_C$ and there's restriction of profunctors along functors. I don't see why this definition is any less "conceptual"

Max New (Nov 07 2022 at 23:55):

Ok, Mike's point about the two different functors makes a lot more sense to me. What I have to consider is in this category theory library is if that would cause any problems?

Nathanael Arkor (Nov 08 2022 at 00:00):

In the end, it is just a matter of personal preference. Neither definitions should cause any problems, since one should easily be able to add ops as needed. So you should just go with whichever you prefer (or you could always poll the other contributors to the repository if you're worried the choice might be controversial) :)

John Baez (Nov 08 2022 at 00:11):

Mike Shulman said:

If you define a profunctor from $C$ to $D$ to be covariant in $D$ and contravariant in $D$,

Typo alert: I think you mean covariant in $C$ and contravariant in $D$.

Christian Williams (Nov 08 2022 at 00:36):

If you want to communicate the basic concept of profunctor, a relation of categories, to ordinary people, you can draw this picture. relation.png Then it is clear that like an ordinary hom, it is "negative" in the first variable and "positive" in the second.

Christian Williams (Nov 08 2022 at 00:40):

I understand there is an interesting perspective for the opposite convention; but I just care about how to share this language with people, so this is the one I will always use.

Christian Williams (Nov 08 2022 at 00:47):

To me, until a concept gains broad understanding and use, conventions are TBD.

Christian Williams (Nov 08 2022 at 01:32):

I think the idea that profunctors are just "homs between categories" is one of the most simple yet illuminating ideas in all of category theory. Cat, in all its richness, is essentially just one huge network of objects and morphisms, grouped into "bubbles" called categories.

Christian Williams (Nov 08 2022 at 01:34):

E.g. In this view, a natural transformation is just a functor between collages.

Christian Williams (Nov 08 2022 at 01:43):

If one wants to base the convention on universal properties, a "global view" of cocompletion as acting on equipments, rather than categories, is given by Mod(-) in Enriched Categories as a Free Cocompletion. Then the above picture is a bimodule in Mod(Span). From this view, I don't know how or why it could be flipped around.

Christian Williams (Nov 08 2022 at 01:53):

I guess I've never asked, what causes this "reversal" between Mod(Mat(Set)) and Prof ~ Kl(Cocomp)?

Christian Williams (Nov 08 2022 at 02:09):

(Also @Nathanael Arkor, a monad is equivalent to a theory by forming Kl(T)^op, right? So the opposite is certainly a natural construction as well.)

Christian Williams (Nov 08 2022 at 02:10):

Mike Shulman said:

Many people find it nicer and more convenient, especially when working abstractly with proarrow equipments from the pseudofunctor perspective, to have one of these functors be "totally covariant".

In string diagrams, having one "op" and one "co" is perfect, because one is rotating clockwise and one counterclockwise. (If you used co-op, it would involve reflection.) comp-conj.png

Mike Shulman (Nov 08 2022 at 04:57):

Christian Williams said:

If one wants to base the convention on universal properties, a "global view" of cocompletion as acting on equipments, rather than categories, is given by Mod(-) in Enriched Categories as a Free Cocompletion. Then the above picture is a bimodule in Mod(Span). From this view, I don't know how or why it could be flipped around.

Exactly, from that perspective it can't be flipped around at all -- and the convention you get that way is the one I'm advocating for, where a profunctor from $C$ to $D$ is covariant in $C$ and contravariant in $D$. You can tell because from that perspective an equipment is a functor like $\rm Cat \to Prof$, which is totally covariant. See Remark 15.7 in that paper.

Mike Shulman (Nov 08 2022 at 05:40):

Here's a purely double-categorical version of the argument. Consider a 2-cell in the double category of profunctors whose boundary consists of profunctors $H: B^{\rm op} \times A \to \rm Set$ and $K:D^{\rm op} \times C \to \rm Set$ and functors $f:A\to C$ and $g:B\to D$. (So far I'm being agnostic about the direction in which $H$ and $K$ are considered to point.) Such a 2-cell has components that are set-functions $H(b,a) \to K(gb,fa)$, so it seems unavoidable that $H$ should be considered a sort of "domain" and $K$ a sort of "codomain".

If you draw the two possible pictures for the two possible orientations of $H$ and $K$, you'll see that if $H$ points from $A$ to $B$ and $K$ from $C$ to $D$, then a 2-cell drawn with $H$ in its domain and $K$ in its codomain must point from a "composite" "$g\circ H$" to a "composite" "$K\circ f$". If we make the opposite choice, then the 2-cell must point from "$f\circ H$" to "$K\circ g$".

However, in the case when $H = \mathrm{Hom}_A$ and $K=\mathrm{Hom}_C$ are identity profunctors (so $B=A$ and $D=C$), a 2-cell of this sort is equivalent to an ordinary natural transformation from $g$ to $f$. Thus, it seems contrary to reason for $f$ to appear in the "domain" of a general such 2-cell and $g$ in the "codomain". Therefore, $H$ must point from $A$ to $B$, and $K$ from $C$ to $D$.

Christian Williams (Nov 08 2022 at 05:55):

Yes, so here is the discrepancy: I think that $h$ and $k$ are morphisms, while what you are calling $f$ and $g$ are part of the transformation $\phi$. I don't think that they should be understood as morphisms. inf.png
(what do you call $a\mapsto fa$, a "mapping instance"?)

Reid Barton (Nov 08 2022 at 06:34):

@Max New, sorry if this is a dumb question for some reason, but if you are concerned about the order that variables appear in a profunctor, couldn't you take a profunctor from $C$ to $D$ to be a functor $F : C \times D^{\mathrm{op}} \to \mathrm{Set}$?

Christian Williams (Nov 08 2022 at 06:38):

As for Mod(-), I neglected to double check your paper. I see now that you define bimodules of lax functors "the other way". So anyway, I understand the reasoning for the Kleisli perspective. I'm only saying the following.

When we actually draw an explicit heteromorphism, polarity $(-,+)$ points "forwards" and $(+,-)$ points "backwards". Precomposition is contravariant and postcomposition is covariant; that is essentially the basic asymmetry of an arrow. You have good reasons for the utility of the opposite convention, but I'm just saying that your $A\times B^{op}\to \mathrm{Set}$ heteromorphisms literally point from $B$ to $A$, as arrows.

Reid Barton (Nov 08 2022 at 06:49):

I sort of feel like there are two intensionally different concepts here (profunctor, and heteromorphism/family of heteromorphisms) that turn out to be equivalent modulo things like variance and ordering of variables (at least when the categories involved are small??) and maybe that accounts for the different preferences.

Reid Barton (Nov 08 2022 at 06:49):

In my opinion, if you're using the word "profunctor", then only the nlab convention on its direction is sensible.

Reid Barton (Nov 08 2022 at 06:50):

I could sort of understand if people were claiming that they really cared more about copresheaf categories or about limit-preserving functors instead of colimit-preserving ones, but no one seems to be claiming that.

Christian Williams (Nov 08 2022 at 07:13):

But this fact is not invertible: precomposition is contravariant, and postcomposition is covariant. There is no "opposite equivalent" of that.

Mike Shulman (Nov 08 2022 at 07:41):

Christian Williams said:

I think that $h$ and $k$ are morphisms, while what you are calling $f$ and $g$ are part of the transformation $\phi$. I don't think that they should be understood as morphisms.

I don't see how one can claim that functors are not a kind of morphism.

Mike Shulman (Nov 08 2022 at 07:47):

Christian Williams said:

I'm just saying that your $A\times B^{op}\to \mathrm{Set}$ heteromorphisms literally point from $B$ to $A$, as arrows.

Yes, that's true: the elements of a profunctor from $A$ to $B$ are "hetero-arrows" from an object of $B$ to an object of $A$. That's the reason for writing $B^{\rm op}\times A \to \rm Set$ rather than $A \times B^{\rm op}\to\rm Set$, so that in $H(b,a)$ the contravariant variable is first just like in a homset. Unfortunately, no convention is absolutely perfect.

Matteo Capucci (he/him) (Nov 08 2022 at 11:01):

Right, I find the heteroarrows idea very powerful for reasoning about profunctors, hence my preference for contravariant-covariant. But y'all making very good points for the opposite convention...

Max New (Nov 08 2022 at 13:22):

Mike Shulman said:

Here's a purely double-categorical version of the argument. Consider a 2-cell in the double category of profunctors whose boundary consists of profunctors $H: B^{\rm op} \times A \to \rm Set$ and $K:D^{\rm op} \times C \to \rm Set$ and functors $f:A\to C$ and $g:B\to D$. (So far I'm being agnostic about the direction in which $H$ and $K$ are considered to point.) Such a 2-cell has components that are set-functions $H(b,a) \to K(gb,fa)$, so it seems unavoidable that $H$ should be considered a sort of "domain" and $K$ a sort of "codomain".

If you draw the two possible pictures for the two possible orientations of $H$ and $K$, you'll see that if $H$ points from $A$ to $B$ and $K$ from $C$ to $D$, then a 2-cell drawn with $H$ in its domain and $K$ in its codomain must point from a "composite" "$g\circ H$" to a "composite" "$K\circ f$". If we make the opposite choice, then the 2-cell must point from "$f\circ H$" to "$K\circ g$".

However, in the case when $H = \mathrm{Hom}_A$ and $K=\mathrm{Hom}_C$ are identity profunctors (so $B=A$ and $D=C$), a 2-cell of this sort is equivalent to an ordinary natural transformation from $g$ to $f$. Thus, it seems contrary to reason for $f$ to appear in the "domain" of a general such 2-cell and $g$ in the "codomain". Therefore, $H$ must point from $A$ to $B$, and $K$ from $C$ to $D$.

I don't follow here. I would define a 2-cell from $H$ to $K$ along $g,f$ as going from $H$ to $K(g, f)$ both considered as functors $B^o \times A \to \textrm{Set}$, I don't know what you mean by saying it must point from $g \circ H$ to $K \circ f$.

Mike Shulman (Nov 08 2022 at 16:38):

Draw the square picture and imagine it as a picture in a 2-category.

Max New (Nov 08 2022 at 16:48):

The codomain of H is Set so what do you mean by $g \circ H$?

Mike Shulman (Nov 08 2022 at 16:49):

We're talking about thinking of profunctors as morphisms between categories. So if $H$ is a morphism from $A$ to $B$, you can imagine "composing" it with $g:B\to D$ even though they're different kinds of morphisms.

Mike Shulman (Nov 08 2022 at 16:51):

square.png

Max New (Nov 08 2022 at 17:00):

Ok I see what you mean but I would prefer we don't think of the left and right in a profunctor as inputs and outputs at all

Christian Williams (Nov 08 2022 at 17:01):

Mike Shulman said:

Christian Williams said:

I think that $h$ and $k$ are morphisms, while what you are calling $f$ and $g$ are part of the transformation $\phi$. I don't think that they should be understood as morphisms.

I don't see how one can claim that functors are not a kind of morphism.

I'm not talking about the whole functor; I mean on the level of elements, because we were discussing heteromorphisms. I'm saying that I think a "mapping instance" $\mapsto$ should not be understood as a heteromorphism $\to$. It's not a "lasting connection", it's a "blink-of-an-eye transformation". inf.png

Mike Shulman (Nov 08 2022 at 17:06):

Max New said:

Ok I see what you mean but I would prefer we don't think of the left and right in a profunctor as inputs and outputs at all

I'm very sympathetic to that. In fact I prefer a sort of "multi-variable" formal category theory where the "modules" can depend on arbitrarily many "categories" without partitioning them into a "domain" and a "codomain". But you're the one who opened this thread by asking about how a profunctor should be oriented!

Mike Shulman (Nov 08 2022 at 17:07):

Christian Williams said:

I'm not talking about the whole functor; I mean on the level of elements, because we were discussing heteromorphisms. I'm saying that I think a "mapping instance" $\mapsto$ should not be understood as a heteromorphism $\to$.

I can see that point, but you said "what you are calling $f$ and $g$", and what I was calling $f$ and $g$ are functors. I was not referring to "mapping instances" at all. So I don't see that this is relevant.

Christian Williams (Nov 08 2022 at 17:42):

Okay, so you were considering a transformation in the case that $H=A(-,-)$ and $K=C(-,-)$. Even though the square may "look like" it's going from $g\circ A$ to $C\circ f$, I think these squares should be interpreted in terms of substitution, so it is really a transformation $A \Rightarrow C(f,g)$. There are equivalent ways of interpreting a transformation $H\Rightarrow K(f,g)$, but I think the simplest interpretation is this cartesian cell.

Mike Shulman (Nov 08 2022 at 18:18):

As I said, I'm very happy to not orient profunctors at all. But the OP was if we orient them, which direction should we orient them.

Mike Shulman (Nov 08 2022 at 18:24):

This $\mathbb{Z}/2$ action on the domain and codomain of a profunctor reminds me of the $\mathbb{Z}/2$ action on the two kinds of morphism in a double category, where some people draw the proarrows horizontally and other vertically. In that case, using the words "tight morphism" and "loose morphism" gives us a way to be unambiguous about which kind of morphism we're talking about, in contrast to "horizontal morphism" and "vertical morphism" that depend on a fairly arbitrary choice of orientation on a page. I wonder whether we could do something similar for the two boundaries of a loose morphism, calling them perhaps the "covariant domain" and "contravariant domain" to be unambiguous independently of which one might be the "source" and which the "target".

Mike Shulman (Nov 08 2022 at 18:28):

Unfortunately when we write something like $H : A ⇸ B$, we have to choose one of the categories to be on the left and the other on the right. But we could consider replacing ⇸ by a different notation that refers directly to covariance and contravariance rather than to a "source" and "target". For instance, if $H$ has covariant domain $A$ and contravariant domain $B$, we could agree that I could write $H : A ⊷ B$ and someone else could write $H : B ⊶ A$, and then each of us could read what the other has written and know immediately what it means without having to check their convention about which is the "source" and which the "target". Since Max's original question referred to developing a library, I wonder whether something like that might also work in a formalization context, akin to defining $a \ge b$ to mean $b \le a$ and allowing individual contributors to use whichever notation they prefer.

Max New (Nov 08 2022 at 19:08):

In the library I'm basically deciding what Prof C D means

Max New (Nov 08 2022 at 19:08):

So there isn't really any directionality implied

Mike Shulman (Nov 08 2022 at 19:12):

Except that you write C first and D second. I don't know of anyone who writes $H : C \leftarrow D$.

Max New (Nov 08 2022 at 21:09):

⊶ and ⊷ is a very nice suggestion, with I guess the opened one being contravariant because it looks like "op". This is completely doable in Agda

Mike Shulman (Nov 08 2022 at 21:23):

Max New said:

I guess the opened one being contravariant because it looks like "op".

Yes, that was my idea.

Tom Hirschowitz (Nov 09 2022 at 10:38):

Mike Shulman said:

Except that you write C first and D second. I don't know of anyone who writes $H : C \leftarrow D$.

Backhouse et al.'s Categorical fixed point calculus uses this convention. I found it extreeeeemely hard to read, albeit not only for this reason.

fosco (Nov 09 2022 at 11:43):

I commit to use ⊶ as the definitive notation for profunctors from today on!

Matteo Capucci (he/him) (Nov 09 2022 at 12:23):

Obligatory question: how do you Latex it?

fosco (Nov 09 2022 at 13:21):

image.png

Mike Shulman (Nov 09 2022 at 17:48):

I'm pleased to see such a positive reaction. Unfortunately the math on this zulip doesn't seem to have a package installed for these characters. For reference, the unicode for ⊶ is U+22B6 ORIGINAL OF and for ⊷ it's U+22B7 IMAGE OF (where do they get these names?).

Matteo Capucci (he/him) (Nov 10 2022 at 10:39):

Unicode names are the most bizarre things lol

Ryan Wisnesky (Nov 10 2022 at 16:12):

apologies if this has been stated before, but I wanted to be sure the database theory point of view is captured: a pro-functor C -|-> D can be thought of a set of conjunctive queries on C, one per object of D, along with query morphisms. So practically speaking, a pro-functor generalizes SQL's "view" mechanism to multiple tables connected by foreign keys. as an engineer I find this connection beautiful and unexpected. (I oriented -|-> in the direction of SQL)

fosco (Nov 10 2022 at 21:45):

As a category theorist, I find this connection beautiful and unexpected, but in hindsight natural (so even more beautiful)!

Valeria de Paiva (Nov 11 2022 at 13:24):

well, using \multimap will conflict with linear implication, maybe not so good?

Mike Shulman (Nov 11 2022 at 16:12):

Neither of the two suggested symbols is \multimap.

Jean-Baptiste Vienney (Nov 11 2022 at 20:57):

fosco said:

image.png

It was suggested here.

Morgan Rogers (he/him) (Nov 11 2022 at 20:59):

I think the highlighting was accidental in that screenshot.

Jean-Baptiste Vienney (Nov 11 2022 at 21:02):

Oh, so the confusion must come from that.

Noah Chrein (Oct 28 2023 at 18:53):

I've been thinking about the intuition that @Christian Williams gave in the picture , that a profunctor is an "abstract representative of morphisms from a:A to b:B", much like the representative morphism for comma categories. (3.4.6 from Emily Riehl's elements) .

It also justifies the notation. The arrow P:A⇸B represents the arrows "inside P" breaking through the "boundary" separating the objects a:A from the objects b:B.

I draw an arrow with 2 bars for an abstract path of profunctors breaking through multiple boundaries. This extends to n bars when you know that a paths of profunctors are part of the data when given $\mathcal V$ : fc-multicategory .

Make this in tikzcd using "{ |^n| }"{marking, allow upside down} it works fast in quiver too.

This "representative" notation idea is not limited to $fc$-multicategories (virtual double categories)

Noah Chrein (Oct 29 2023 at 19:21):

Figured out how to draw an easy profunctor in KaTeX (which is zulip), as well as my notiation for paths of profunctors:

$\mathrlap{\;+}\to$ \mathrlap{\;+}\to $\mathrlap{+\!\!\!+}\to$ \mathrlap{+\!\!\!+}\to

you can use other symbols than +, like \shortmid if you'd like, but this is more to type

Mike Shulman (Oct 29 2023 at 19:47):

Or you can just use the unicode ⇸.

Matteo Capucci (he/him) (Oct 30 2023 at 09:10):

Noah Chrein said:

It also justifies the notation. The arrow P:A⇸B represents the arrows "inside P" breaking through the "boundary" separating the objects a:A from the objects b:B.

This never occurred to me, cool!