English
If left zigzag equals the standard left unitor-trace for f, then the right zigzag equals the standard right unitor-trace for g for an equivalence e.
Русский
Если левый зигзаг равен стандартному следу левых униторов для f, тогда правый зигзаг равен стандартному следу правых униторов для g для некой эквивалентности e.
LaTeX
$$$\\left( \\text{leftZigzag }\\eta.hom\\,\\varepsilon.hom = (\\lambda_{f})^{\\mathrm{hom}} \\;\\circ\\; (\\rho_{f})^{-1} \\right) \\Rightarrow \\left( \\text{rightZigzag }\\eta.hom\\,\\varepsilon.hom = (\\rho_{g})^{\\mathrm{hom}} \\;\\circ\\; (\\lambda_{g})^{-1} \\right)$$$
Lean4
theorem right_triangle_of_left_triangle (h : leftZigzag η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv) :
rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv :=
by
rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]
calc
_ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
_ = rightZigzag η.hom ε.hom := (rightZigzag_idempotent_of_left_triangle _ _ h)
_ = _ := by simp
