Commit 2025-02-27 22:45 04fb392f

feat(CategoryTheory): 2-squares of functors (#22248) Adds a type TwoSquare T L B R of natural transformation across the diagonal of a commutative square of functors, including operations for whiskering on the sides of the square and for pasting squares vertically and horizontally. We use this type to refactor the notion of Guitart exactness and of adjoint mates.