English
Naturality of the inverse left unitor with respect to middle whiskering: (λ_f)^{-1} ◁ g equals (α_ (𝟙 a) f g)^{hom}⁻¹ ≫ (λ_{f ≫ g})^{-1}.
Русский
Натурализм обратного левого уитора по отношению к среднему висению.
LaTeX
$$$ (\\lambda_f)^{-1} \\triangleleft g = (\\alpha_{\\mathbf{1}_a} f g)^{hom^{-1}} \\; ≫ \\; (\\lambda_{f \\gg g})^{-1} $$$
Lean4
@[reassoc, simp]
theorem whiskerLeft_rightUnitor_inv (f : a ⟶ b) (g : b ⟶ c) : f ◁ (ρ_ g).inv = (ρ_ (f ≫ g)).inv ≫ (α_ f g (𝟙 c)).hom :=
eq_of_inv_eq_inv
(by simp)
/-
It is not so obvious whether `leftUnitor_whiskerRight` or `leftUnitor_comp` should be a simp
lemma. Our choice is the former. One reason is that the latter yields the following loop:
[id_whiskerLeft] : 𝟙 a ◁ (ρ_ f).hom ==> (λ_ (f ≫ 𝟙 b)).hom ≫ (ρ_ f).hom ≫ (λ_ f).inv
[leftUnitor_comp] : (λ_ (f ≫ 𝟙 b)).hom ==> (α_ (𝟙 a) f (𝟙 b)).inv ≫ (λ_ f).hom ▷ 𝟙 b
[whiskerRight_id] : (λ_ f).hom ▷ 𝟙 b ==> (ρ_ (𝟙 a ≫ f)).hom ≫ (λ_ f).hom ≫ (ρ_ f).inv
[rightUnitor_comp] : (ρ_ (𝟙 a ≫ f)).hom ==> (α_ (𝟙 a) f (𝟙 b)).hom ≫ 𝟙 a ◁ (ρ_ f).hom
-/
