2-commutative squares of functors #
CommSq.lean defines the notion of commutative squares,
this file introduces the notion of 2-commutative squares of functors.
T : C₁ ⥤ C₂,
L : C₁ ⥤ C₃,
R : C₂ ⥤ C₄,
B : C₃ ⥤ C₄ are functors,
[CatCommSq T L R B] contains the datum of an isomorphism
T ⋙ R ≅ L ⋙ B.
Future work: using this notion in the development of the localization of categories (e.g. localization of adjunctions).
the isomorphism corresponding to a 2-commutative diagram
CatCommSq T L R B expresses that there is a 2-commutative square of functors, where
B are respectively the left, top, right and bottom functors
of the square.
[CatCommSq T L R B],
iso T L R B is the isomorphism
T ⋙ R ≅ L ⋙ B
given by the 2-commutative square.
Horizontal composition of 2-commutative squares
Vertical composition of 2-commutative squares
Horizontal inverse of a 2-commutative square
In a square of categories, when the top and bottom functors are part of equivalence of categorires, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.