English
Let f: a → b and g: b → c be 1-morphisms in a bicategory. Then the hom component of the right unitor for f ≫ g is given by the composite of the associator with the identity on c whiskered by f and the right unitor of g: (ρ_{f ≫ g}).hom = (α_{f,g,(𝟙 c)}).hom ≫ f ◁ (ρ_g).hom.
Русский
Пусть f: a → b и g: b → c — 1-морфизмы в бикатегории. Тогда гом-компонента правого унитора для f ≫ g равна композиции ассоциатора с единицей на c, взятой по горизонтальному обводу слева через f, с правым унитором g: (ρ_{f ≫ g}).hom = (α_{f,g,(𝟙 c)}).hom ≫ f ◁ (ρ_g).hom.
LaTeX
$$$ (\\rho_{f \\gg g}).hom = (\\alpha_{f g \\mathbf{1}_c}).hom \\;\\gg\\; f \\;◁\\; (\\rho_g).hom $$$
Lean4
@[reassoc]
theorem rightUnitor_comp (f : a ⟶ b) (g : b ⟶ c) : (ρ_ (f ≫ g)).hom = (α_ f g (𝟙 c)).hom ≫ f ◁ (ρ_ g).hom := by simp
