English
Dual right naturality for the inverse of the associator: f ◁ g ◁ η with α_f g h'.inv equals α_f g h.inv followed by (f ≫ g) ◁ η.
Русский
Двойной правый натурализм для обратного ассоциатора: тождество между двумя способами применения η к f и g через обратный ассоциатор.
LaTeX
$$$ f ◁ g ◁ η \\; \\circ \\; (α_f g h')^{-1} = (α_f g h)^{-1} \\circ (f ≫ g) ◁ η $$$
Lean4
/-- We state it as a simp lemma, which is regarded as an involved version of
`id_whiskerRight f g : 𝟙 f ▷ g = 𝟙 (f ≫ g)`.
-/
@[reassoc, simp]
theorem leftUnitor_whiskerRight (f : a ⟶ b) (g : b ⟶ c) : (λ_ f).hom ▷ g = (α_ (𝟙 a) f g).hom ≫ (λ_ (f ≫ g)).hom := by
rw [← whiskerLeft_iff, whiskerLeft_comp, ← cancel_epi (α_ _ _ _).hom, ← cancel_epi ((α_ _ _ _).hom ▷ _),
pentagon_assoc, triangle, ← associator_naturality_middle, ← comp_whiskerRight_assoc, triangle,
associator_naturality_left]
