Repository navigation
Define composition of polynomial functors #56
Description
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 compFunctorIso), however (but it might be nice to add it anyway to have a more complete library of polynomial functor facts). (CC @u5943321)
Activity
sinhp commentedon Feb 19, 2025
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 commentedon Sep 19, 2025
Exponentiability is proven in sinhp/Poly#34.