Home for cartesian natural transformations?

Stream: mathlib4

[Sina Hazratpour 𓃵]

I had a bit of difficulty finding where cartesian natural transformations are in mathlib. Apparently they are known in mathlib by their other name "equifibered transformations" which is totally fine, but they are located in the file CategoryTheory.Limits.VanKampen. Isn't the file NatTrans a more natural home for them? Other than Van Kampen colimits they also show up in double-categorical mates, polynomial functors and cartesian monads among other things.

[Kim Morrison]

Yes, feel free to move them to a new file.