We present a formalism for Petri nets based on polynomial-style finite-set
configurations and etale maps. The formalism supports both a geometric
semantics in the style of Goltz and Reisig (processes are etale maps from
graphs) and an algebraic semantics in terms of free coloured props: the Segal
space of P-processes is shown to be the free coloured prop-in-groupoids on P.
There is also an unfolding semantics \`a la Winskel, which bypasses the
classical symmetry problems. Since everything is encoded with explicit sets,
Petri nets and their processes have elements. In particular, individual-token
semantics is native, and the benefits of pre-nets in this respect can be
obtained without the need of numberings. (Collective-token semantics emerges
from rather drastic quotient constructions \`a la Best--Devillers, involving
taking $\pi_0$ of the groupoids of states.)