#### Howdy, Stranger!

It looks like you're new here. If you want to get involved, click one of these buttons!

Options

# Open Petri nets

edited August 2018

My student Jade Master and I have just finished a paper on open Petri nets:

• John Baez and Jade Master, Open Petri nets.

Abstract. The reachability semantics for Petri nets can be studied using open Petri nets. For us an 'open' Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category, which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$. Various choices of semantics for open Petri nets can be described using symmetric monoidal double functors out of $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$. Here we describe the reachability semantics, which assigns to each open Petri net the relation saying which markings of the outputs can be obtained from a given marking of the inputs via a sequence of transitions. We show this semantics gives a symmetric monoidal lax double functor from $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$ to the double category of relations. A key step in the proof is to treat Petri nets as presentations of symmetric monoidal categories; for this we use the work of Meseguer, Montanari, Sassone and others.

I've started blogging about it here:

There's a lot of applied category theory in here. We build a symmetric monoidal category where the morphisms are open Petri nets, like this:

But actually do much more: we build a symmetric monoidal double category. A double category has two types of arrows, which go horizontally and vertically, and also squares:

We use the squares to describe maps between open Petri nets.

• Options
1.

Very cool! I can't wait to see the paper, although it will take me a while to puzzle my way through the ideas of a double category.

Comment Source:Very cool! I can't wait to see the paper, although it will take me a while to puzzle my way through the ideas of a double category.
• Options
2.
edited August 2018

The paper is here now:

Abstract. The reachability semantics for Petri nets can be studied using open Petri nets. For us an 'open' Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category, which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$. Various choices of semantics for open Petri nets can be described using symmetric monoidal double functors out of $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$. Here we describe the reachability semantics, which assigns to each open Petri net the relation saying which markings of the outputs can be obtained from a given marking of the inputs via a sequence of transitions. We show this semantics gives a symmetric monoidal lax double functor from $$\mathbb{O}\mathbf{pen}(\mathrm{Petri})$$ to the double category of relations. A key step in the proof is to treat Petri nets as presentations of symmetric monoidal categories; for this we use the work of Meseguer, Montanari, Sassone and others.

Comment Source:The paper is here now: * John Baez and Jade Master, [Open Petri nets](http://math.ucr.edu/home/baez/petri.pdf) > **Abstract.** The reachability semantics for Petri nets can be studied using open Petri nets. For us an 'open' Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category, which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category \$$\mathbb{O}\mathbf{pen}(\mathrm{Petri})\$$. Various choices of semantics for open Petri nets can be described using symmetric monoidal double functors out of \$$\mathbb{O}\mathbf{pen}(\mathrm{Petri})\$$. Here we describe the reachability semantics, which assigns to each open Petri net the relation saying which markings of the outputs can be obtained from a given marking of the inputs via a sequence of transitions. We show this semantics gives a symmetric monoidal lax double functor from \$$\mathbb{O}\mathbf{pen}(\mathrm{Petri})\$$ to the double category of relations. A key step in the proof is to treat Petri nets as presentations of symmetric monoidal categories; for this we use the work of Meseguer, Montanari, Sassone and others. 
• Options
3.
edited August 2018

Scott - our paper is not very good for learning what a double category is! In particular we need 'pseudo double categories', where composition of horizontal arrows is associative only up to an 'associator' 2-morphism. It's easiest to start with 'strict' double categories.

I suspect the most fun place to start is Eugenia Cheng's video:

But she seems to be assuming you've already watched a video on internal categories, which I can't find.

Comment Source:Scott - our paper is not very good for learning what a double category is! In particular we need 'pseudo double categories', where composition of horizontal arrows is associative only up to an 'associator' 2-morphism. It's easiest to start with 'strict' double categories. I suspect the most fun place to start is Eugenia Cheng's video: * The Catsters, [Double categories](https://www.youtube.com/watch?v=kiCZiSA2W3Q&feature=channel_page). But she seems to be assuming you've already watched a video on internal categories, which I can't find. 
• Options
4.

Yeah, I knew you would be assuming readers already have the background. When reading math I don't know much about, it can take a while for things to click. If I read something and don't understand everything, I keep reading to get what I can and come back later when I am wiser.

I suspect the most fun place to start is Eugenia Cheng's video:

The Catsters, Double categories.

But she seems to be assuming you've already watched a video on internal categories, which I can't find.

The Catster's is great and I will watch that video, although I get a lot more out of it from doing this course and reading some from Tom Leinster's book and Emily Riehl's book. My only complaint is (like you found) that the video's seemed to have been made with some sort of order in my mind, but it's not clear what order that is. But I am sure I can find the definition for internal categories on wikipedia or nLab.

Comment Source:Yeah, I knew you would be assuming readers already have the background. When reading math I don't know much about, it can take a while for things to click. If I read something and don't understand everything, I keep reading to get what I can and come back later when I am wiser. > I suspect the most fun place to start is Eugenia Cheng's video: >> The Catsters, Double categories. > But she seems to be assuming you've already watched a video on internal categories, which I can't find. The Catster's is great and I will watch that video, although I get a lot more out of it from doing this course and reading some from Tom Leinster's book and Emily Riehl's book. My only complaint is (like you found) that the video's seemed to have been made with some sort of order in my mind, but it's not clear what order that is. But I am sure I can find the definition for internal categories on wikipedia or nLab. 
• Options
5.

The videos were not made with an order in mind! We made videos on things we wanted to make videos about. "I feel like making some videos about x today!" That's how we kept the enthusiasm and the energy. The project would have collapsed quite quickly if we felt we had to slog through topics in some specific order. So the videos are not supposed to form a linear course as such, but are supposed to help you understand various things in category theory. :-)

Anyway, there's Brent Yorgey's Catsters guide that you might find useful.

Comment Source:The videos were not made with an order in mind! We made videos on things we wanted to make videos about. "I feel like making some videos about x today!" That's how we kept the enthusiasm and the energy. The project would have collapsed quite quickly if we felt we had to slog through topics in some specific order. So the videos are not supposed to form a linear course as such, but are supposed to help you understand various things in category theory. :-) Anyway, there's Brent Yorgey's [Catsters guide](https://byorgey.wordpress.com/catsters-guide-2/) that you might find useful.
• Options
6.
edited August 2018

What's the difference between a double category and a bicategory?

Comment Source:What's the difference between a double category and a bicategory?
• Options
7.
edited August 2018

According to nLab:

If $$\mathcal{C}$$ is a 2-category, there is its double category of squares $$\mathrm{Sq}(\mathcal{C})$$ whose objects are those of $$\mathcal{C}$$, both of whose types of morphisms are the morphisms in $$\mathcal{C}$$, and whose squares are 2-morphisms in $$\mathcal{C}$$ with their source and target both decomposed as a composite of two morphisms. (These squares are sometimes called quintets $$(\alpha,f,g,h,k)$$ where $$\alpha\colon f g \to h k$$, and so this double category is said to be a quintet construction.)

so it sounds like any bicategory is a special case of a double category.

Comment Source:According to nLab: > If \$$\mathcal{C}\$$ is a 2-category, there is its double category of squares \$$\mathrm{Sq}(\mathcal{C})\$$ whose objects are those of \$$\mathcal{C}\$$, both of whose types of morphisms are the morphisms in \$$\mathcal{C}\$$, and whose squares are 2-morphisms in \$$\mathcal{C}\$$ with their source and target both decomposed as a composite of two morphisms. (These squares are sometimes called *quintets* \$$(\alpha,f,g,h,k)\$$ where \$$\alpha\colon f g \to h k\$$, and so this double category is said to be a quintet construction.) so it sounds like any bicategory is a special case of a double category. 
• Options
8.
edited August 2018

Functors and profunctors form a double category actually.

In fact, I wouldn't be surprised if $$\mathcal{V}$$-functors and $$\mathcal{V}$$-profunctors form something like a double $$\mathcal{V}$$-category.

Comment Source:Functors and profunctors form a double category actually. In fact, I wouldn't be surprised if \$$\mathcal{V}\$$-functors and \$$\mathcal{V}\$$-profunctors form something like a double \$$\mathcal{V}\$$-category.
• Options
9.
edited August 2018

So bicategories are double categories where A and B are the same category?

Comment Source:So bicategories are double categories where A and B are the same category?
• Options
10.
edited August 2018

Christopher wrote:

So bicategories are double categories where A and B are the same category?

Not quite, though there's indeed a nice way to get a bicategory from a double category having this property.

Bicategories and double categories provide two ways to enhance the concept of category by including '2-morphisms'. In a bicategory the 2-morphisms are shaped like bigons:

In a double category the 2-morphisms are shaped like squares:

The direction of the double arrow in the middle of this square is unimportant; that's a purely artistic issue.

In a double category the vertical 1-morphisms can be completely different from the horizontal 1-morphisms. In a bicategory there is only one kind of 1-morphism. In both cases there are geometrically plausible ways to compose these 2-morphisms.

There are various ways to get double categories from bicategories and vice versa. Indeed, if you have a double category whose vertical 1-morphisms are exactly the same, with the same rule of composition, as the horizontal 1-morphisms, you can use this fact to get a bicategory with those 1-morphisms.

You can also get a bicategory from any double category, using another obvious trick.

Conversely, Scott mentioned a way to get a double category from a bicategory. Let me enhance his nLab quote slightly:

If $$\mathcal{C}$$ is a bicategory, there is its double category of squares $$\mathrm{Sq}(\mathcal{C})$$ whose objects are those of $$\mathcal{C}$$, both of whose types of morphisms are the morphisms in $$\mathcal{C}$$, and whose squares are 2-morphisms in $$\mathcal{C}$$ with their source and target both decomposed as a composite of two morphisms. (These squares are sometimes called quintets $$(\alpha,f,g,h,k)$$ where $$\alpha\colon f g \to h k$$, and so this double category is said to be a quintet construction.)

I recommend this as a very quick and sketchy introduction to such issues; it won't answer all your questions but it will sketch the landscape:

• John Baez, An introduction to n-categories, in 7th Conference on Category Theory and Computer Science, eds. Eugenio Moggi and Giuseppe Rosolini, Lecture Notes in Computer Science vol. 1290, Springer, Berlin, 1997.
Comment Source:Christopher wrote: > So bicategories are double categories where A and B are the same category? Not quite, though there's indeed a nice way to get a bicategory from a double category having this property. Bicategories and double categories provide two ways to enhance the concept of category by including '2-morphisms'. In a bicategory the 2-morphisms are shaped like **bigons**: <center><img src = "http://math.ucr.edu/home/baez/mathematical/7_sketches/2-cell_bicategory.png"></center> In a double category the 2-morphisms are shaped like squares: <center><img src = "http://math.ucr.edu/home/baez/mathematical/7_sketches/2-cell_double_category.png"></center> The direction of the double arrow in the middle of this square is unimportant; that's a purely artistic issue. In a double category the vertical 1-morphisms can be completely different from the horizontal 1-morphisms. In a bicategory there is only one kind of 1-morphism. In both cases there are geometrically plausible ways to compose these 2-morphisms. There are various ways to get double categories from bicategories and vice versa. Indeed, if you have a double category whose vertical 1-morphisms are exactly the same, with the same rule of composition, as the horizontal 1-morphisms, you can use this fact to get a bicategory with those 1-morphisms. You can also get a bicategory from _any_ double category, using _another_ obvious trick. Conversely, Scott mentioned a way to get a double category from a bicategory. Let me enhance his nLab quote slightly: > If \$$\mathcal{C}\$$ is a bicategory, there is its double category of squares \$$\mathrm{Sq}(\mathcal{C})\$$ whose objects are those of \$$\mathcal{C}\$$, both of whose types of morphisms are the morphisms in \$$\mathcal{C}\$$, and whose squares are 2-morphisms in \$$\mathcal{C}\$$ with their source and target both decomposed as a composite of two morphisms. (These squares are sometimes called *quintets* \$$(\alpha,f,g,h,k)\$$ where \$$\alpha\colon f g \to h k\$$, and so this double category is said to be a quintet construction.) I recommend this as a very quick and sketchy introduction to such issues; it won't answer all your questions but it will sketch the landscape: * John Baez, [An introduction to n-categories](http://arxiv.org/abs/q-alg/9705009), in _7th Conference on Category Theory and Computer Science_, eds. Eugenio Moggi and Giuseppe Rosolini, Lecture Notes in Computer Science vol. 1290, Springer, Berlin, 1997.
• Options
11.
edited August 2018

Keith wrote:

Functors and profunctors form a double category actually.

Yeah, that's a great example of a double category!

In fact, I wouldn't be surprised if $$\mathcal{V}$$-functors and $$\mathcal{V}$$-profunctors form something like a double $$\mathcal{V}$$-category.

Maybe so! But it's actually less stressful to think of them as forming a plain old double category $$\mathbb{P}\mathbf{rof}_\mathcal{V}$$:

• There's a category $$\mathbf{Cat}_\mathcal{V}$$ with $$\mathcal{V}$$-categories as objects and $$\mathcal{V}$$-functors as morphisms. We can use this as the vertical category of our double category.

• There's a category $$\mathbf{Prof}_\mathcal{V}$$ with $$\mathcal{V}$$-categories as objects and $$\mathcal{V}$$-profunctors as morphisms. We can use this as the horizontal category of our double category.

Then we have to figure out what the squares (i.e. 2-morphisms) should be in the double category $$\mathbb{P}\mathbf{rof}_\mathcal{V}$$. They should be natural transformations! We want $$a$$ here to be a natural transformation from $$gf$$ to $$i h$$:

But for that to make sense, we need to answer two questions in the $$\mathcal{V}$$-enriched setting:

• what's a natural transformation between profunctors?

• how do we compose a functor and a profunctor to get a profunctor?

We've already seen how to answer the second question: just take the companion of your functor, to turn it into a profunctor, so you can compose it with a profunctor and get another profunctor!

The first question is also pretty easy to answer.

And here's a really cool fact: the concepts of 'companion' and 'conjoint' can be defined in any double category! They may not always exist, but you can define them, so you can check to see if they exist. In $$\mathbb{P}\mathbf{rof}_\mathcal{V}$$, they exist and they match the notions we've already seen in this class!

Another nice double category is $$\mathbb{R}\mathbf{el}$$. This sets as objects, functions as vertical morphisms and relations as horizontal morphisms. There are two obvious ways to turn a function into a relation, and in the double category $$\mathbb{R}\mathbf{el}$$ these turn out to be its companion and conjoint.

You can read a detailed description of $$\mathbb{R}\mathbf{el}$$ in Section 5 of my paper Open Petri nets. See page 72 of Mike Shulman's paper for the general definition of companion and conjoint.

Comment Source:Keith wrote: > Functors and profunctors form a double category actually. Yeah, that's a great example of a double category! > In fact, I wouldn't be surprised if \$$\mathcal{V}\$$-functors and \$$\mathcal{V}\$$-profunctors form something like a double \$$\mathcal{V}\$$-category. Maybe so! But it's actually less stressful to think of them as forming a plain old double category \$$\mathbb{P}\mathbf{rof}_\mathcal{V}\$$: * There's a category \$$\mathbf{Cat}_\mathcal{V}\$$ with \$$\mathcal{V}\$$-categories as objects and \$$\mathcal{V}\$$-functors as morphisms. We can use this as the vertical category of our double category. * There's a category \$$\mathbf{Prof}_\mathcal{V}\$$ with \$$\mathcal{V}\$$-categories as objects and \$$\mathcal{V}\$$-profunctors as morphisms. We can use this as the horizontal category of our double category. Then we have to figure out what the squares (i.e. 2-morphisms) should be in the double category \$$\mathbb{P}\mathbf{rof}_\mathcal{V}\$$. They should be natural transformations! We want \$$a\$$ here to be a natural transformation from \$$gf\$$ to \$$i h\$$: <center><img src = "http://math.ucr.edu/home/baez/mathematical/7_sketches/2-cell_double_category.png"></center> But for that to make sense, we need to answer two questions in the \$$\mathcal{V}\$$-enriched setting: * what's a natural transformation between profunctors? * how do we compose a functor and a profunctor to get a profunctor? We've already seen how to answer the second question: just take the _companion_ of your functor, to turn it into a profunctor, so you can compose it with a profunctor and get another profunctor! The first question is also pretty easy to answer. And here's a really cool fact: the concepts of 'companion' and 'conjoint' can be defined in _any_ double category! They may not always exist, but you can define them, so you can check to see if they exist. In \$$\mathbb{P}\mathbf{rof}_\mathcal{V}\$$, they exist and they match the notions we've already seen in this class! Another nice double category is \$$\mathbb{R}\mathbf{el}\$$. This sets as objects, functions as vertical morphisms and relations as horizontal morphisms. There are two obvious ways to turn a function into a relation, and in the double category \$$\mathbb{R}\mathbf{el}\$$ these turn out to be its companion and conjoint. You can read a detailed description of \$$\mathbb{R}\mathbf{el}\$$ in Section 5 of my paper [Open Petri nets](http://math.ucr.edu/home/baez/petri.pdf). See page 72 of [Mike Shulman's paper](https://arxiv.org/abs/0706.1286) for the general definition of companion and conjoint. 
• Options
12.
edited August 2018

This explains the reachability semantics for open Petri nets as a map between double categories.

Comment Source:Here's another blog article about my paper with Jade Master: * [Open Petri nets (post 2)](https://johncarlosbaez.wordpress.com/2018/08/18/open-petri-nets-part-2/). This explains the reachability semantics for open Petri nets as a map between double categories.
• Options
13.
edited August 2018

And here's the third and final part:

This explains how to get symmetric monoidal categories from Petri nets!

Sorry folks, I had to blog about this paper to get it out of my system - it's full of fun stuff, but it's eaten up energy that I'd otherwise spend writing lectures here. Now that's done!

Comment Source:And here's the third and final part: * [Open Petri nets (post 3)](https://johncarlosbaez.wordpress.com/2018/08/19/open-petri-nets-part-3/). This explains how to get symmetric monoidal categories from Petri nets! Sorry folks, I had to blog about this paper to get it out of my system - it's full of fun stuff, but it's eaten up energy that I'd otherwise spend writing lectures here. Now that's done!
• Options
14.
edited August 2018

Oh man, I was really confused. I thought '2 category' meant what bicategory means, and 'bicategory' what double category actually means.

So this also answers the question I tried to answer in the other thread. The full sub double category of Prof_V whose objects are the discrete V-preorders is equivalent to the double category of sets, functions on those sets, and linear functions between vector spaces over V, with basis the set.

Correct?

Comment Source:Oh man, I was really confused. I thought '2 category' meant what bicategory means, and 'bicategory' what double category actually means. So this also answers the question I tried to answer in the other thread. The full sub double category of Prof_V whose objects are the discrete V-preorders is equivalent to the double category of sets, functions on those sets, and linear functions between vector spaces over V, with basis the set. Correct? 
• Options
15.
edited August 2018

A 2-category is a bicategory where the associator and unitor 2-morphisms

$$\alpha_{f,g,h} \colon (f \circ g) \circ h \Rightarrow f \circ (g \circ h)$$ $$\lambda_f \colon 1 \circ f \Rightarrow f$$ $$\rho_f \colon f \circ 1 \Rightarrow f$$ are identity 2-morphisms. A bicategory is the same as a double category where all vertical 1-morphisms are identity morphisms.

The full sub double category of $$\mathbf{Prof}_\mathcal{V}$$ whose objects are the discrete $$\mathcal{V}$$-preorders is equivalent to the double category of sets, functions on those sets, and linear functions between vector spaces over $$\mathcal{V}$$, with basis the set.

Correct?

Something like this is probably true, but let me try to understand your terminology!

• You didn't say here, but I'll assume you're using $$\mathcal{V}$$ to mean a commutative quantale since that's what we've been doing in the class.

• We never talk about a "$$\mathcal{V}$$-preorder" — we talk about $$\mathcal{V}$$-enriched categories, or $$\mathcal{V}$$-categories, for short. Is that what you're talking about? I'll assume so.

• I've never discussed "discrete" $$\mathcal{V}$$-enriched categories, but I can guess by analogy with discrete preorders that these have $$\mathcal{X}(x,y) = I$$ (the unit for multiplication in our quantale) when $$x = y$$ and $$\mathcal{X}(x,y) = \bot$$ (the bottom element of our quantale). I think this should give a well-defined $$\mathcal{V}$$-enriched category for any choice of the set of objects.

• Nobody ever talks about "vector spaces" over commutative quantale, just over fields. But a commutative quantale is a kind of rig, which is a generalization of a ring, which is a generalization of a field. So if someone started talking about a vector space over $$\mathcal{V}$$ with a given set as basis, I'd assume they meant the free $$\mathcal{V}$$-module over that set. That's the right generalization of a vector space to this context.

After making these interpretations, I think you're right! I think there should indeed be a double category with

• discrete $$\mathcal{V}$$-enriched categories as objects

• $$\mathcal{V}$$-enriched functors as vertical 1-morphisms

• $$\mathcal{V}$$-enriched profunctors as horizontal 1-morphisms

• natural transformations as 2-morphisms

and also a double category with

• sets as objects

• functions between these sets as vertical 1-morphisms

• $$\mathcal{V}$$-module morphisms between the free $$\mathcal{V}$$-modules on these sets as horizontal 2-morphisms

• some sort of 2-morphisms

and these should be equivalent... if you pick the right 2-morphisms for the second one.

Comment Source:A 2-category is a bicategory where the associator and unitor 2-morphisms $\alpha_{f,g,h} \colon (f \circ g) \circ h \Rightarrow f \circ (g \circ h)$ $\lambda_f \colon 1 \circ f \Rightarrow f$ $\rho_f \colon f \circ 1 \Rightarrow f$ are identity 2-morphisms. A bicategory is the same as a double category where all vertical 1-morphisms are identity morphisms. > The full sub double category of \$$\mathbf{Prof}_\mathcal{V}\$$ whose objects are the discrete \$$\mathcal{V}\$$-preorders is equivalent to the double category of sets, functions on those sets, and linear functions between vector spaces over \$$\mathcal{V}\$$, with basis the set. > Correct? Something like this is probably true, but let me try to understand your terminology! * You didn't say here, but I'll assume you're using \$$\mathcal{V}\$$ to mean a commutative quantale since that's what we've been doing in the class. * We never talk about a "\$$\mathcal{V}\$$-preorder" &mdash; we talk about \$$\mathcal{V}\$$-enriched categories, or \$$\mathcal{V}\$$-categories, for short. Is that what you're talking about? I'll assume so. * I've never discussed "discrete" \$$\mathcal{V}\$$-enriched categories, but I can guess by analogy with discrete preorders that these have \$$\mathcal{X}(x,y) = I\$$ (the unit for multiplication in our quantale) when \$$x = y\$$ and \$$\mathcal{X}(x,y) = \bot\$$ (the bottom element of our quantale). I think this should give a well-defined \$$\mathcal{V}\$$-enriched category for any choice of the set of objects. * Nobody ever talks about "vector spaces" over commutative quantale, just over fields. But a commutative quantale is a kind of [rig](https://en.wikipedia.org/wiki/Semiring), which is a generalization of a ring, which is a generalization of a field. So if someone started talking about a vector space over \$$\mathcal{V}\$$ with a given set as basis, I'd assume they meant the free \$$\mathcal{V}\$$-module over that set. That's the right generalization of a vector space to this context. After making these interpretations, I think you're right! I think there should indeed be a double category with * discrete \$$\mathcal{V}\$$-enriched categories as objects * \$$\mathcal{V}\$$-enriched functors as vertical 1-morphisms * \$$\mathcal{V}\$$-enriched profunctors as horizontal 1-morphisms * natural transformations as 2-morphisms and also a double category with * sets as objects * functions between these sets as vertical 1-morphisms * \$$\mathcal{V}\$$-module morphisms between the free \$$\mathcal{V}\$$-modules on these sets as horizontal 2-morphisms * some sort of 2-morphisms and these should be equivalent... if you pick the right 2-morphisms for the second one.