English
For any functor H:E→C, any natural transformation α:F⇒G between F,G:C→D, the X-th component of the horizontal whiskering with id_H equals α evaluated at H(X): (id_H ◫ α)_X = α_{H(X)}.
Русский
Для любого функторa H:E→C и натур трансформации α:F⇒G между F,G:C→D, компонент X-й горизонтальной зашивки с id_H равен α на H(X): (id_H ◫ α)_X = α_{H(X)}.
LaTeX
$$$ (\mathrm{Id}_H \; ◫ \; α)_X = α_{H(X)} $$$
Lean4
theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by
simp
-- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we
-- need to use associativity of functor composition. (It's true without the explicit associator,
-- because functor composition is definitionally associative,
-- but relying on the definitional equality causes bad problems with elaboration later.)
