leftUnitor_hom_congr — Mathlib

English

If h : f = f' then left whiskering with eqToHom h relates the two left whiskers.

Русский

Если h : f = f', то левое взвешивание через eqToHom h связывает два левых whisker-случая.

LaTeX

$$$(λ_ f).hom = 𝟙 _ ◁ eqToHom h ≫ (λ_ f').hom ≫ eqToHom h.symm$$$

Lean4

theorem leftUnitor_hom_congr {x y : B} {f f' : x ⟶ y} (h : f = f') :
    (λ_ f).hom = 𝟙 _ ◁ (eqToHom h) ≫ (λ_ f').hom ≫ eqToHom h.symm :=
  by
  subst h
  simp

Похожие утверждения