English
Provide an isomorphism between F.op.mapTriangle and the inverse triangleOpEquivalence composed with F.mapTriangle.op, i.e. an iso between F.op.mapTriangle and (triangleOpEquivalence C).inverse ⋅ F.mapTriangle.op.
Русский
Обеспечивается изоморфизм между F.op.mapTriangle и (triangleOpEquivalence C).inverse ⋅ F.mapTriangle.op.
LaTeX
$$$F.op.mapTriangle \cong (\triangleOpEquivalence C)^{-1} \circ F.mapTriangle.op$$$
Lean4
/-- Vertical inverse of the 2-commutative square of
`CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor`.
-/
noncomputable instance :
CatCommSq (F.op.mapTriangle) (triangleOpEquivalence C).inverse (triangleOpEquivalence D).inverse F.mapTriangle.op :=
CatCommSq.vInv (F.mapTriangle.op) (triangleOpEquivalence C) (triangleOpEquivalence D) F.op.mapTriangle inferInstance
