Define composition of polynomial functors

[Vtec234]

In the blueprint, it is definition 5.0.6. The construction is here in the Poly package, but we haven't proven that the resulting map is exponentiable. A sketch of the proof is in Mark Weber's Polynomials in Categories with Pullbacks.

We need this to define the interpretation of Sigma types (here). It seems we do not need the isomorphism $P_{f▸g} ≅ P_f ∘ P_g$ (compFunctorIso), however (but it might be nice to add it anyway to have a more complete library of polynomial functor facts). (CC @u5943321)

[sinhp]

And as a warm-up exercise leading to the isomorphism @Vtec234 mentioned, it might be a good idea to establish that isomorphism in the category of types where things are more concrete:

https://github.com/sinhp/Poly/blob/0740abde64b16779ab031e1c2cad61b929c9b32d/Poly/Type/Univariate.lean#L224

UPDATE: This special case has now been completed here.

[Vtec234]

Exponentiability is proven in sinhp/Poly#34.