Morphism of Polynomial Functors

Let P , Q 𝑃 𝑄 P,Q be a pair of Polynomial Functors. A morphism of polynomial functors P → Q → 𝑃 𝑄 P\to Q consists of:

  1. A function f : P ⁢ ( 1 ) → Q ⁢ ( 1 ) : 𝑓 → 𝑃 1 𝑄 1 f:P(1)\to Q(1)
  2. A function f ♯ : ( p : P ( 1 ) ) → Q [ f ( p ) ] → P [ p ] f^{\sharp}:(p:P(1))\to Q[f(p)]\to P[p]

Note that these are simply morphisms in ∫ Fam ⁢ ( Sets ) op Fam superscript Sets op \int\mathrm{Fam}(\mathrm{Sets})^{\mathrm{op}} , EG: the Total Category of the the Fibrewise Opposite of the Family Fibration over the Category of Sets.