I have defined the Beck-Chevalley natural transformations, but not shown that they are isomorphisms. Links [`MorphismProperty.Over.map` /left adjoint to pb/sigma](https://github.com/sinhp/HoTTLean/blob/168533908807c8d5811976b02e09820a54f78501/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean#L107) and [pushward/right adjoint to pb/pi](https://github.com/sinhp/HoTTLean/blob/168533908807c8d5811976b02e09820a54f78501/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean#L175)
I have defined the Beck-Chevalley natural transformations, but not shown that they are isomorphisms. Links
MorphismProperty.Over.map/left adjoint to pb/sigma and pushward/right adjoint to pb/pi