Morphisms of polynomial endofunctors

[fredrik-bakke]

Additions

• morphisms and natural transformations of polynomial endofunctors
• show morphisms are a retract of natural transformations
• universal property of cartesian morphisms of arrows
• cartesian morphisms and cartesian natural transformations of polynomial endofunctors
• univalent polynomial endofunctors
• construct underlying global subuniverse of univalent type families and univalent polynomial endofunctors

[fredrik-bakke]

Alright, I'm marking this as ready for review now. I didn't manage to prove all the things I had initially planned to. As it turns out, the original goals are probably just not provable. At least some partial results are proven, and some other useful results are added.