English
In any bicategory, the right unitor and the associator satisfy a triangle identity linking the right whiskering of a 1-morphism with the inverse of the left unitor of the identity and the associator. Specifically, for any 1-morphisms f: a → b and g: b → c, the equality between the two 2-cells (ρ_f)^{-1} whiskered by g followed by α_f(I_b, g)^{hom} and f whiskered by (λ_g)^{-1} holds.
Русский
В любой бисистеме категорий тождество треугольника связывает правый уитор с ассоциатором: для любых 1-морфизмов f: a → b и g: b → c справедливо равенство между (ρ_f)^{-1} ∘_право g затем α_f(𝟙_b, g)^{hom} и f ◁ (λ_g)^{-1}.
LaTeX
$$$ (\\rho_f)^{-1} \\triangleright g \\; \\circ \\; (\\alpha_f(\\mathbf{1}_b, g))_{\\mathrm{hom}} = f \\triangleright (\\lambda_g)^{-1} $$$
Lean4
@[reassoc (attr := simp)]
theorem triangle_assoc_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) : (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv :=
by simp [← cancel_mono (f ◁ (λ_ g).hom)]
