Commit 2024-07-30 16:14 53c5e956

feat(CategoryTheory): preservation of pullback/pushout squares (#15044) The main result in this PR is that a commutative square sq : Square C is a pullback square iff it is mapped to a pullback square in the category of types when we apply the functor coyoneda.obj X for any X : Cᵒᵖ. In order to do this, it is shown that the proprety Square.IsPullback is preserved when a functor preserving this pullback is applied. A similar result is obtained for pushout squares, which required developing the "opposites" API for squares.