Commit 2025-07-05 08:08 a1126145

feat(CategoryTheory/Limits/Pullback/Categorical): categorical cospan transforms (#26412) This PR adds API for transformations of "categorical cospan transforms", i.e unbundled pseudonatural transformations of cospans of objects in the 2-category of categories. Although we cannot state it this way because we work with unbundled objects, these form a bicategory, and this encodes the data required to properly state bifunctoriality of the categorical pullback defined in #26366.