`MorphismProperty.Over.map` /left adjoint to pb/sigma preserves pullbacks. [Here](https://github.com/sinhp/HoTTLean/blob/168533908807c8d5811976b02e09820a54f78501/HoTTLean/ForMathlib/CategoryTheory/Polynomial.lean#L480) The LCC proof (which I think is entirely analogous) already exists somewhere - either in Poly or already in Mathlib.
