Define mapping from cartesian squares to cartesian natural transformations between polynomial functors #55

Formalize Definition 5.0.9 in the blueprint. In Poly, this is defined in cartesianNaturalTrans, but we haven't yet shown that this is actually cartesian (all naturality squares are pullbacks). (CC @u5943321) An internal proof of this is proposition 2.1.7 in Kock.

We need this to lift Pi formation from universe-monomorphic to universe-polymorphic as described here.