English
Let F be a pseudofunctor between bicategories. For any objects b0 and b1 and any morphism f: b0 → b1, the hom-component of the two-cell mapComp' at (id b0, f, f) is determined by the left unitor and the map of the identity at b0; specifically it is the composition of the inverse left unitor with the inverse of mapId b0, whiskered appropriately by F.map f.
Русский
Пусть F — псевдофунктор между бикатегориями. Для любых объектов b0, b1 и морфизма f: b0 → b1 гом-компонента 2-ячейки mapComp' в сочетании (id b0, f, f) задаётся когерентностью через обратный левый юнитор и отображение единицы: это композиция обратного левого юнитора с обратной самостоятельной отображением id(b0), учтённая через взвешивание справа F.map f.
LaTeX
$$$(F.mapComp' (\\mathrm{id}_{b_0})\\, f\\, f).hom = (\\lambda_{F b_0})^{-1} \\\\; ≫ (F.mapId b_0)^{-1} \\\\; ▷ \\, F.map f$$$
Lean4
@[to_app (attr := reassoc)]
theorem mapComp'_id_comp_hom {b₀ b₁ : B} (f : b₀ ⟶ b₁) :
(F.mapComp' (𝟙 b₀) f f).hom = (λ_ _).inv ≫ (F.mapId b₀).inv ▷ _ := by simp [mapComp'_id_comp]
