Cartesian Morphism of Polynomial Functors

A cartesian morphism of polynomial functors is a Cartesian Morphism in the Category of Polynomial Functors. More explicitly, it is a morphism of polynomial functors ( f , f ♯ ) : P → Q : 𝑓 superscript 𝑓 ♯ → 𝑃 𝑄 (f,f^{\sharp}):P\to Q such that f ♯ superscript 𝑓 ♯ f^{\sharp} is an equivalence.

This can easily be seen by studying the Cartesian Morphisms of the Family Fibration, recalling that Poly = Fam ⁢ ( Sets op ) Poly Fam superscript Sets op \mathrm{Poly}=\mathrm{Fam}(\mathrm{Sets}^{\mathrm{op}}) .