{'fraction_non_alphanumeric': 0.05548260013131976, 'fraction_numerical': 0.00443204202232436, 'mean_word_length': 3.820541224877354, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Categorical Semantics for Guarded Petri Nets

We build on the correspondence between Petri nets and free symmetric strict monoidal categories already investigated in the literature, and present a categorical semantics for Petri nets with guards. This comes in two flavors: Deterministic and with side-effects. Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself.


Introduction
Category theory has been used to study Petri nets at least since the beginning of the nineties [7]. Throughout this time, the main effort in this direction of research consisted in showing how Petri nets can be thought of as presenting various flavors of free monoidal categories [3, 6,7,9] This idea has been very influential, successfully modeling the individual-token philosophy via process semantics.
On the other hand, shortly after Petri's first publications about the nets that carry his name [8] researchers started investigating what happens when nets are enriched with new features. One of the most successful extensions of Petri nets is guarded (or coloured) nets [4]. Modulo different flavors of modeling what boils down to be the same concept, a guarded net is a Petri net with the following extra properties: -To each token is attached some "attribute". The kind of attributes we can attach to tokens depends on the place the token is in; -Each arc is decorated with an expression, which modifies tokens' attributes as they flow through the net; -Each transition is decorated with a predicate and only fires on tokens whose attributes satisfy the predicate.
At a fist glance, guarded nets allow for a more expressive form of modeling with respect to their unguarded counterparts, but as we will see shortly, this is not necessarily the case. Indeed, depending on the underlying theory from which properties, expressions, and predicates are drawn the gain in expressive power with respect to undecorated nets may be nil: With a wise choice of underlying theory, coloured nets amount to be nothing more than syntactic sugar for standard nets, though of course the availability of such syntactic sugar can greatly simplify the modeling of complex processes using the Petri net formalism.
Recently there has been renewed interest in employing Petri nets as the basis for a programming language [11]. In this setting, the categorical correspondence between nets and symmetric monoidal categories has been of the utmost importance, single-token philosophy being considered necessary to make the programming language usable [10]. Clearly, extending nets with new features such as guards or timings is desirable to make the language more expressive.
In this work we try to unify these two longstanding directions of researchthe categorical approach to Petri nets and the study of guarded nets -by showing how guarded nets can be modeled as ordinary Petri nets with a particular flavor of semantics in the style of [1].
Importantly, we are able to define both a deterministic semantics and a nondeterministic semantics in our formalism. The first models the traditional notion of guards deterministically modifying data attached to tokens, while the second describes a setting where token data is modified depending on side effects.
Using the Grothendieck construction, we show how the guard semantics can be internalized in the net itself, providing a categorical proof that in our model, guarded nets do not increase expressivity, as compared to traditional nets. This is a desired feature, since it means that many nice properties of nets such as termination or decidability of the reachability relation are preserved. It also shows that the core mathematical abstraction in computer implementations of Petri nets need not be modified when offering users the flexibility of guarded nets.
We save all proofs for the appendix, which starts on page 14.

Guarded nets
Having given an intuitive version of what a guarded net is, we now start modeling the concept formally. We will use the formalism developed in [1], of which we recall some core concepts. We denote by F (N ) the free symmetric strict monoidal category associated to a Petri net N , and with U (C) the petri net associated to the free symmetric strict monoidal category C. We denote composition in diagrammatic order; i.e. given f : c → d and g : d → e, we denote their composite by (f g) : c → e. Definition 1. Given a strict monoidal category S, a Petri net with S-semantics is a pair N, N ♯ , consisting of a Petri net N and a strict monoidal functor Nets equipped with S-semantics and their morphisms form a monoidal category denoted Petri S , with the monoidal structure arising from the product in Cat.
Definition 2. We denote by Set * the category of sets and partial functions, and by Span the 1-category of sets and spans, where isomorphic spans are identified. Both these categories are symmetric monoidal. From now on, we will work with the strictified version of Set * and Span, respectively. Example 1. Let 1 denote the terminal symmetric monoidal category. A Petri net with 1-semantics is just a Petri net. Petri nets are in bijective correspondence with free symmetric strict monoidal categories, so Petri 1 denotes the usual category of free symmetric strict monoidal categories and strict monoidal functors between them.
Notation 1. Recall that a morphism A → B in Span consists of a set S and a pair of functions A ← S → B. When we need to notationally extract this data from f , we write We sometimes consider the span as a function f : Perhaps unsurprisingly, Set * and Span will be the target semantics corresponding to two different flavors for our guards, with Span allowing for some form of nondeterminism -expressed as the action of side-effects -whereas Set * models a purely deterministic semantics. Expressing things formally: Definition 3. A guarded net is an object of Petri Set * . A guarded net with side effects is an object of Petri Span . A morphism of guarded nets (with side effects) is a morphism in Petri Set * (resp. in Petri Span ).
Remark 1. Although it doesn't affect our formalism by any means, in practice the choice of semantics, both for Set * and Span, is limited by computational requirements: the places in a net are usually sent to finite sets, while transitions are usually sent to computable functions and spans 3 , respectively. Such restrictions are necessary to make sure the net is executable and to keep model checking decidable.
Let us unroll the cryptic Definition 3, starting from the case Petri Set * . An object in Petri Set * is a net N together with a strict monoidal functor N ♯ : F (N ) → Set * . It assigns to each place p of N -corresponding to a generating object of F (N ) -a set N ♯ (p), representing all the possible colours a token in p can assume. A transition f : p → p ′ -corresponding to a generating morphism of F (N ) -gets sent to a partial function N ♯ (f ) : N ♯ (p) → N ♯ (p ′ ), representing how token colours are transformed during firing. Importantly, the fact that the functions in the semantics are partial means that a transition may not be defined for tokens of certain colors. An example of this is the net in Fig. 1a, which is shown together with its semantics. Although reachability in the base net seems quite straightforward, we see that a token in the leftmost place will never reach the rightmost place, since the rightmost transition is not defined on the tokens output by the leftmost one.
In the case of Petri Span the intuition is similar. Objects are sent to sets, exactly as in Petri Set * , but transitions are mapped to spans. Spans can be understood as relations with witnesses, provided by elements in the apex of the span. Practically, this means that each path from the span domain to its codomain is indexed by some element of the span apex, as it is shown in Fig. 1b. The presence of witnesses allows to consider different paths between the same elements. Moreover, an element in the domain can be sent to different elements in the codomain via different paths. We interpret this as non-determinism: The firing of the transition is not only a matter of the tokens input and output, it also includes the path chosen, which we interpret as having side-effects that are interpreted outside of our model. As one can see, in both Figs. 1a and 1b the  composition of paths is the empty function (resp. span). Seeing things from a reachability point of view, the process given by firing the left transition and then the right will never occur. Let us make this intuition precise: Definition 4. Given a guarded Petri net (with side effects) N, N ♯ , a marking for N, N ♯ is a pair (X, x) where X is an object of F (N ) and x ∈ N ♯ X. We say that a marking (Y, y) is reachable from The goal we will pursue in the next section will be to internalize the guard semantics in the free category F (N ) associated to a net.

Internalizing guards
By "internalizing the semantics of a guarded net N in F (N )" we mean obtaining an unguarded net M such that F (M ) represents all the possible runs of N . For readers familiars with coloured Petri nets, this corresponds to the claim that reachability in a coloured net is equivalent to reachability in a suitably constructed "standard" net [4].
Since our point of view is process-theoretic, and we are working with symmetric strict monoidal categories and functors, such internalization must be built categorically. The main tool we will use is the Grothendieck construction [5], which in our context we will specialize to functors to Set * and Span, respectively. Definition 5. Let M, M ♯ ∈ Petri Set * be a guarded net. We define its internalization, denoted M ♯ , as the following category: -The objects of M ♯ are pairs (X, x), where X is an object of F (M ) and x is an element of M ♯ X. Concisely: It is worth giving some intuition of what the Grothendieck construction does in our context. It basically makes a place for each element of the set we send a place to, and makes a transition for each path between these elements, as shown below: An equivalent definition exists when the semantics is taken to be in Span, which is the following: Definition 6. Let M, M ♯ ∈ Petri Span be a guarded net with side effects. We define the internalization of M, M ♯ , denoted with M ♯ , as the following category: -The objects of M ♯ are pairs (X, x), where X is an object of F (M ) and x is an element of M ♯ X. Concisely: and s ∈ S M ♯ f in the apex of the corresponding span connects x to y. Concisely: The intuition in the span case is exactly as for partial functions, and we don't deem it useful to draw the same picture again. Looking at the example, though, a couple of things become clear. The first is that to justify the idea of the Grothendieck construction turning an assignment of semantics into a net we have to prove that the resulting category is symmetric strict monoidal and free. The second is that the net thus built is fibered over the base net, and there should be an opposite construction sending M ♯ to M . Both of these claims are true, as we now prove: Lemma 1. In the case of both Set * and Span, the category M ♯ has a strict symmetric monoidal structure.
Theorem 1. In both the case of Set * and of Span the strict symmetric monoidal category M ♯ is free.
There is an equality f 1 g 1 = f 2 g 2 as morphisms (X, x) → (Z, z) in M ♯ , proving M ♯ is not free. The reason that Theorem 1 holds in the span case is that spans keep track of different paths between elements, whereas relations do not. To see this, consider the span composition: It is clear that in this composition the two paths from x to z are considered as separated in the Span case, and witnessed by y 1 , y 2 respectively, while in the case of Rel they would have been conflated to one. The result is that these paths correspond to the same morphism in the relational case of M ♯ , introducing new equations and breaking freeness, while they stay separated in the span case.
Lemma 2. In the case of both Set * and Span, there is a strict monoidal functor Remark 2. In general, π M is not an opfibration. This is because our target categories Set * and Span allow for partial functions. Indeed, if f : X → Y in M is sent by M ♯ to a partial function that is not defined on x ∈ M ♯ X, then there is no coCartesian lift emanating from (X, x) for the morphism f .
We conclude this section by proving that the reachability semantics of a guarded net coincides with the reachability semantics of its internalization.

Properties of internalizations
The Grothendieck construction provides a way to internalize partial function and span semantics to nets. As such, it acts on objects of the categories Petri Set * and Petri Span , respectively. It is thus worth asking what happens to morphisms in these categories. The answer is, luckily, easy to find: , such that the following diagram on the left (resp. on the right) commutes: The notation for the liftings in Lemma 3 is easy to remember: The arrow over ⇀ F looks like a stylized function, while the hat over F looks like a sylized span.
The lifting of Lemma 3 is quite well-behaved. First of all, it is worth stressing how it preserves some relevant categorical properties: Having ascertained that "basic" categorical properties are preserved, it is worth asking what happens to particular classes of functors in Petri Set * and Petri Span , respectively.
Following [1], there are three relevant kinds of morphisms in a category of Petri nets with semantics. On one hand there are transition-preserving functors, which represent morphisms of free monoidal categories arising purely from the topological structure of their underlying net. On the other there are functors representing glueings of nets, which are themselves divided into synchronizations (defined in terms of addition and erasing of generators, that is, double pushouts) and identifications (defined in terms of pushouts). Let us investigate which ones of these properties are preserved.
Definition 7. A strict symmetric monoidal functor F between FSSMCs C, D is said to be transition-preserving when each generating morphism f of C is mapped to σ g σ ′ for some generating morphism g of D and symmetries σ, σ ′ .
Identifications are also preserved. The ultimate reason for this is that identifications are defined purely in terms of coequalizers of transition-preserving functors, which are preserved by the Grothendieck construction. Preservation of identifications also entails that both additions and erasings of generators for a net are preserved by internalizations.
which sends generating objects to generating objects, is injective on objects and faithful; where W denotes the net with the same places of W and no transitions; and -M ♯ arises from the universal property of the pushout. Lemma 8. Let M, M ♯ be an addition of generating morphisms to K, K ♯ via W, w. Then M ♯ is an addition of generating morphisms to K ♯ via U (w K ♯ ) , ⇀ w. The span case is analogous.
where N w denotes the net with the same places of N w and no transitions, is a subnet of K, K ♯ ; and Lemma 9. Let K, K ♯ be an erasing of generating morphisms from N, N ♯ via a subnet N w . Then K ♯ is an erasing of generators from N ♯ via sub Nw N ♯ . The span case is analogous.
Surprisingly, even if erasing and addition of generators are preserved by internalizations, synchronizations are not. Indeed, following with w factorizing through w ′ . In internalizing this construction the pushouts are preserved, but the rewrite rule is not! This becomes evident by lifting the definition of synchronization altogether, where in the following diagram we are sticking to the notation developed in [1]: The black arrows are just the definition of synchronization. The dotted arrows denote the pushout arrows, while the dashed arrows arise from the universal property of the pushout. The maroon arrows and objects represent the Grothendieck construction and the lifting of the functors obtained from Lemma 3, while the πs stand for the functors obtained in Lemma 2, where we omitted subscripts to avoid clutter. As one can see the pushout squares are both preserved, but M ♯ is not a synchronization of N ♯ via in W w N ♯ since In other words, sub Nw N ♯ is too big of a subcategory of N ♯ to make M ♯ into a synchronization. An analogous observation holds for spans.
Counterexample 2 (Synchronizations not preserved). We provide a practical counterexample of why synchronizations are not preserved by internalizations. Consider the following nets, where we are borrowing the graphical notation developed in [1], decorating net elements with their images in Set * .
At the base level we have two nets, M on the left and N on the right. Eliding the functor N ♯ , the places of N are mapped to sets: While transitions are mapped to partial functions f : X → Y and g : Y → Z, defined as follows: f (x) = y 1 g(y 1 ) = g(y 2 ) = z M is clearly a synchronization of N via F : The generators f and g have been erased and a generator corresponding to f g has been added. Taking the Grothendieck construction on M and N (top left and top right in the figure, respectively), we see how the erasing of generators is problematic: The morphism g in N branches into g(y 1 ) and g(y 2 ) in N ♯ , of which only g(y 1 ) forms a path with f (x). In lifting the synchronization M to M ♯ , we would expect g(y 1 ) and f (x) to be erased and conflated into f (x) g(y 1 ), whereas g(y 2 ) stays. But this is not the case, since in M the generator g has already been erased "before being allowed to branch", taking g(y 2 ) with it when we take M ♯ ! As we said before, this ultimately depends on the fact that the internalization of the subnet provided by the synchronization witness contains too many morphisms, and ends up erasing more generators than we would like it to.

Internalization as a functor
In this final section, we put together some of the properties we have proved so far about internalizations, and prove that internalization is a functor. The intuitive argument behind the results that are about to follow is this: If N ♯ internalizes the semantics of N, N ♯ , in either the case N ♯ : N → Set * or N ♯ : N → Span, then N ♯ should be considered as "just a net", that is, an object of Petri 1 ; see Example 1.
Putting together results about lifting of functors obtained in the previous section, we are indeed able to prove this.
Finally, it is worth nothing that for each choice of semantics S there is another obvious functor from Petri S to Petri 1 , which just forgets the semantics altogether. It is worth asking how this functor and the ones provided in Theorem 3 are related.
for Span emb Span

Conclusion and future work
In this work, we described guarded Petri nets as Petri nets endowed with a functorial semantics. We provided two different styles of semantics: a deterministic one, realized using the category of sets and partial functions, and a non-deterministic one that allows for side effects, realized using the category of partial functions and that of spans. We moreover showed how, using the Grothendieck construction, the guards can be internalized, obtaining a Petri net whose reachability relation is equivalent to the one of the guarded one. We proved that internalizations have nice properties, and the internalization construction is functorial in the choice of the guarded net we start from.
Regarding directions of future work, a pretty straightforward thing to do would be to figure out which semantics, other than Set * and Span, are internalizable. That is, if F : F (N ) → S is a symmetric monoidal functor, which properties do S and F need to have so that F is a free symmetric strict monoidal category.

Acknowledgements
David Spivak acknowledges support from Honeywell Inc. as well as from AFOSR grants FA9550-17-1-0058 and FA9550-19-1-0113. Fabrizio Genovese wants to thank his fellow team members at Statebox for useful discussion and support.

Appendix -Proofs
Lemma 1. In the case of both Set * and Span, the category M ♯ has a strict symmetric monoidal structure.
Proof. We start with the case of Set * . Since M ♯ is strict monoidal, M ♯ (X ⊗Y ) = M ♯ X × M ♯ Y . Thus on objects, we can set (X, x) ⊗ (Y, y) := (X ⊗ Y, (x, y)). On morphisms, we just use the monoidal product f ⊗ g from F (M ). The monoidal unit is (I, * ), where I is the monoidal unit of F (M ) and * is the unique element of the monoidal unit { * } of Set * . First, we have to prove that ( )⊗( ) is well-defined, namely that if f : (X, x) → (X ′ , x ′ ) and g : (Y, y) → (Y ′ , y ′ ) then M ♯ (f ⊗ g)(x, y) = (x ′ , y ′ ). This is obvious since M ♯ is strict, therefore: Bifunctoriality of ( ) ⊗ ( ) follows trivially from the fact that it is defined as in F (M ). Moreover, for each object (X, x) we have: (X, x) ⊗ (I, * ) = (X ⊗ I, (x, * )) = (X, (x, * )) = (X, x) (I, * ) ⊗ (X, x) = (I ⊗ X, ( * , x)) = (X, ( * , x)) = (X, x) Where the rightmost equality in each line follows from the fact that we are working with the strictified version of Set * . This proves that unitors are identities. A similar reasoning can be applied to associators, concluding the proof. Now we consider the case of Span. On objects, we set again (X, x) ⊗ (Y, y) := (X ⊗ Y, (x, y)). On morphisms, we set (f, s) ⊗ (g, t) := (f ⊗ g, (s, t)), where f ⊗ g is as in F (M ) and (s, t) is the pair of span-apex elements: The monoidal unit is (I, * ), where I is the monoidal unit of F (M ) and * is the unique element of the monoidal unit { * } of Span. First, we have to prove that the monoidal product ( ) ⊗ ( ) is well-defined, , y), (x ′ , y ′ )). This is obvious since M ♯ is strict, therefore: , y), (x ′ , y ′ )).
The remainder of the proof is as in the previous case.
Theorem 1. In both the case of Set * and of Span the strict symmetric monoidal category M ♯ is free.
Proof. We start with the case of Set * . Consider the free symmetric strict monoidal categoryM generated as follows: -Object generators are pairs (X, x), with X object generator in F (M ) and x ∈ M ♯ X; We want to prove thatM and M ♯ are isomorphic. First, let (X, x) be an object in M ♯ . Then X is an object of F (M ), which is free, and hence we have X = X 1 ⊗ . . . ⊗ X n for generating objects X 1 . . . X n in F (M ). By definition, we have x ∈ M ♯ X. Being M ♯ strict, this means: Hence (X, x) = (X 1 , x 1 ) ⊗ . . . ⊗ (X n , x n ), and the object generators of M ♯ are the pairs (X, x) with X object generator in F (M ) and x ∈ M ♯ X. This means that there is a bijection on objects ofM and M ♯ : We can then define a symmetric monoidal functor T :M → M ♯ that is bijective on objects, and sends a generating morphism f : (X, x) → (Y, y) ofM to the morphism f : (X, x) → (Y, y) in M ♯ .
We want to prove that T is full and faithful. Faithfulness is obvious; given f 1 , f 2 : (X, x) → (Y, y) inM , if T (f 1 ) = T (f 2 ) then in particular f 1 = f 2 in F (M ). It follows from the fact that M ♯ is at most single-valued -i.e. M ♯ g(x) = x ′ and M ♯ g(x) = x ′′ imply x ′ = x ′′ -that f 1 = f 2 also inM .
By definition, since F (M ) is free, any morphism f : X → Z can be decomposed into a composition of monoidal products of morphism generators, symmetries and identities. The points above prove that f : (X, x) → (Z, z) can be decomposed in the same way, and hence is in the image of T ; thus it is full. Our correspondence is bijective on objects and fully faithful, proving thatM and M ♯ are isomorphic as categories. SinceM is free so is M ♯ , completing the proof.
We now consider the case of Span. The structure of the proof is similar. Consider the free symmetric strict monoidal categoryM generated as follows: -Object generators are pairs (X, x), with X object generator in F (M ) and x ∈ M ♯ X; -For each morphism generator f : X → Y and s ∈ S such that M ♯ f (s) = (x, y), there is a morphism generator (f, s) : (X, x) → (Y, y).
We want to prove thatM and M ♯ are isomorphic. On objects, the proof of bijectivity is as in the previous case. We can then define a symmetric monoidal functorM → M ♯ that is bijective on objects, and sends a generating morphism (f, s) : We want to prove that this functor is full and faithful. Faithfulness is again straightforward. Suppose given (f 1 , s 1 ), (f 2 , s 2 ) : (X, x) → (Y, y) inM . By construction, (f 1 , s 1 ) = (f 2 , s 2 ) in M ♯ if and only if f 1 = f 2 in F (M ) and s 1 = s 2 . But this means that (f 1 , s 1 ) = (f 2 , s 2 ) also inM .
By definition, since F (M ) is free, any morphism f can be decomposed into a composition of monoidal products of morphism generators, symmetries and identities. The points above prove that each of such morphisms is also in M ♯ , and hence inM . So f in M ♯ is the image of f inM , and the functor is full.
Since our correspondence is bijective on objects and fully faithful, this proves thatM and M ♯ are isomorphic as categories. SinceM is free so is M ♯ , completing the proof.
Lemma 2. In the case of both Set * and Span, there is a strict monoidal functor π M : M ♯ → F (M ) sending a object (X, x) to X and a morphism f : Proof. Let us prove the statement in the case of Set * , Span being analogous. In M ♯ , the identity on (X, x) is id X : (X, x) → (X, x), which obviously gets sent to id X : X → X in F (M ). Similarly, the monoidal unit (I, * ) of M ♯ is sent to I, which is the monoidal unit of F (M ).
Compositon and tensor product are defined by freeness both in M ♯ and F (M ), and since if f is a generator in M ♯ then it is a generator in F (M ), we have that f ; g (resp. f ⊗ g) in M ♯ is sent to f ; g (resp. f ⊗ g) in F (M ). Strictness follows by definition, concluding the proof.
Again by definition, this means that f : (X, x) → (Y, y) (resp. f s : (X, x) → (Y, y)) is a morphism of N ♯ . Since N ♯ is free, f (resp. f s ) can be decomposed as a composition of monoidal products of generating morphisms. But every generating morphism of N ♯ corresponds to a transition of U N ♯ , from which the thesis follows.
Lemma 3. Let F : M, M ♯ → N, N ♯ be a morphism in Petri Set * (resp. in Petri Span ). Then it lifts to strict monoidal functor ⇀ F : M ♯ → N ♯ (resp. F : M ♯ → N ♯ ), such that the following diagram on the left (resp. on the right) commutes: So ⇀ F acts monoidally on objects. On morphisms, we send f : Proof. We start from ⇀ F . For faithfulness, consider f, g : (X, x) → (Y, y). By definition, Then the corresponding f in F (N ) is a morphism F X → F Y , and since F is full, there is a g : X → Y in F (M ) such that F g = f . Moreover, we have that Now we focus on F . For faithfulness, suppose given (f, s), (g, t) : (X, x) → (Y, y); they are equal iff f = g and s = t. By definition,F (f, s) = (F f, s) andF (g, t) = (F g, t), and henceF (f, s) =F (g, t) iff F f = F g in F (N ) and s = t. Thus F is faithful iffF is faithful. Now suppose F is full, and consider (f, s) : Then the corresponding f in F (N ) is a morphism F X → F Y , and since F is full, there is a g : Clearly it isF (g, s) = (F g, s) = (f, s), proving thatF is full and concluding the proof. Proof. The proof is obvious considering that, by construction, f : (X, x) → (Y, y) is a generator (resp. a symmetry) in N ♯ if and only if it is a generator (resp. a symmetry) in F (N ).
An analogous argument holds for F .

Lemma 6.
If F is injective on objects, so are y). By definition, this means (F X, x) = (F Y, y), from which it follows that x = y and F X = F Y . Since F is injective on objects, then X = Y and so (X, x) = (Y, y), proving that ⇀ F is injective on objects as well.
The span case is analogous. From the first point we get that l M ♯ = r M ♯ , so we can consider: We need to prove that In Span the proof on objects in analogous. On morphisms, notice that since ⇀ l (f, s) = (lf, s) (resp. ⇀ r (f, s) = (rf, s) ) requiring ≃ m ′ to be the equivalence relation on GenMor M ♯ defined by ∀f ∈ GenMor ( l M ♯ ).((f l , s) = (f r , s)) We have that, whenever they exist, (f, s) ≃ m ′ (g, s) in GenMor M ♯ iff f ≃ m g in GenMor F (M ). Considering that (f, s) exists in GenMor M ♯ if and only if [f ] m exists in GenMor N ♯ , we have proven that: The rest of the proof proceeds as in the Set * case. Lemma 8. Let M, M ♯ be an addition of generating morphisms to K, K ♯ via synchronization witness W, w. Then M ♯ is an addition of generating morphisms to K ♯ via synchronization witness U (w K ♯ ) , ⇀ w. The span case is analogous.
Proof. To prove this, consider the following commutative diagram, where we use the notation developed in [1]: The dotted arrows are a pushout, and can be characterized as identifications on the coproduct. We proved in 7 that identifications are preserved, while we defer the proof that coproducts are preserved in the proof of Threorem 3. Hence, M ♯ is the pushout of ⇀ in W and ⇀ in W ⇀ w. The claim follows immediately by noticing that: which is obvious since F W and F (W ) coincide on generating objects and F W has no generating morphisms. Lemma 9. Let K, K ♯ be an erasing of generating morphisms from N, N ♯ via a subnet N w . Then K ♯ is an erasing of generators from N ♯ via sub Nw N ♯ . The span case is analogous.
Proof. The proof is easy by considering the following diagram: Again, the black arrows are the definition of erasing of generators, and are a pushout square. This can be characterized as the coequalizer or a coproduct, where all the morphisms involved are transition-preserving. The maroon objects and arrows are given by the Grothendieck construction and preserve the pushout. The thesis follows by noticing that: Theorem 3. Denote with 1 the terminal category, together with the trivial symmetric monoidal structure on it. There is a faithful, strong monoidal functor emb Span : Petri Set * → Petri 1 defined as follows: Then we have to prove that emb Set * (F ⊗ G) = emb Set * F ⊗ emb Set * G. Unrolling definitions this amounts to prove that G, which is obvious. Finally, we need to prove that emb Set * preserves the monoidal unit. Notice that for each choice of semantics S the monoidal unit in Petri S is taken to be (∅, ∅ ♯ S). F (∅) is the free category consisting of only the monoidal unit I, and ∅ ♯ S : F (∅) → S sends the monoidal unit to the monoidal unit and its identity to itself. In our case, the monoidal unit of Petri Set * is (∅, ∅ ♯ ), with ∅ ♯ sending the monoidal unit of F (∅) to the singleton set { * } in Set * . In particular, this means that ∅ ♯ ≃ F (∅), proving that