English
Let B be a bicategory. If f and f' : x → y are equal, then the inverse of the right unitor at f is obtained from the inverse at f' by transporting along the equality and whiskering with the identity on y; i.e., ρ_f^{-1} equals eqToHom(h) ≫ ρ_{f'}^{-1} ≫ eqToHom(h)^{-1} whiskered by 𝟙_y.
Русский
Пусть B — бикатегория. Для проекции ρ_f на правой единице, если две стрелки f, f' : x → y равны, то обратный правый унитор на f получается из обратного на f' посредством переносa по равенству и ослабления по единичной стрелке на y; то есть ρ_f^{-1} = eqToHom(h) ≫ ρ_{f'}^{-1} ≫ eqToHom(h)^{-1} ▷ 𝟙_y.
LaTeX
$$$\rho_f^{-1} = (eqToHom(h)) \; ≫ \; (\rho_{f'})^{-1} \; ≫ \; (eqToHom(h))^{-1} \; \rhd \; \mathrm{Id}_{y}$$$
Lean4
theorem rightUnitor_inv_congr {x y : B} {f f' : x ⟶ y} (h : f = f') :
(ρ_ f).inv = (eqToHom h) ≫ (ρ_ f').inv ≫ eqToHom h.symm ▷ 𝟙 _ :=
by
subst h
simp
