English
Define an isomorphism between F.op.mapTriangle and triangleOpEquivalence inverses composed with F.mapTriangle.op, giving a 2-commutative square.
Русский
Задаётся изоморфизм между F.op.mapTriangle и (triangleOpEquivalence C).inverse ⋅ F.mapTriangle.op, образующий 2-отклоняющий квадрат.
LaTeX
$$$F.op.mapTriangle \; ⋅ (triangleOpEquivalence C).inverse \cong (triangleOpEquivalence D).inverse ⋅ F.mapTriangle.op$$$
Lean4
/-- If `F : C ⥤ D` commutes with shifts, this is the 2-commutative square of categories
`CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor`.
-/
noncomputable instance :
CatCommSq (F.mapTriangle.op) (triangleOpEquivalence C).functor (triangleOpEquivalence D).functor F.op.mapTriangle :=
⟨F.mapTriangleOpCompTriangleOpEquivalenceFunctor⟩
