Category of arrows and cartesian squares

Stream: maths

[Sina Hazratpour 𓃵]

Is the category of arrows and cartesian squares, a wide subcategory of Arrow C, defined somewhere in mathlib? It's not hard to define it, just wondering if I can import it from somewhere if already done. Also, this is not a full subcategory, and I noticed we don't have Subcategory, only Fullsubcategory.

[Adam Topaz]

We do have docs#WideSubquiver and docs#CategoryTheory.IsPullback . Combining those two, it should be relatively easy to define what you need.

[Sina Hazratpour 𓃵]

i was thinking the same, IsPullback is the way to go. Do you think it is worth adding Widesubcategory and Cart C construction as a wide subcategory to mathlib?

[Adam Topaz]

Yes, I do. And not just Cart but also CoCard and BiCart

[Sina Hazratpour 𓃵]

I'm thinking of naming the file CartSq or CartesianSq. Any suggestion on this is welcome. Also, where would be a good place for it?
Arrow is in CategoryTheory.Comma. That is one option.
CommSq is in CategoryTheory. It can also go to CategoryTheory.