Colored Petri Nets are Lax Double Functors