English
Let F be a pseudofunctor between bicategories B and C. Given composable 1-cells f01: b0 → b1, f12: b1 → b2, f23: b2 → b3, and their composites f02 = f01 ≫ f12, f13 = f12 ≫ f23, along with f = f02 ≫ f23, and the equalities h02: f01 ≫ f12 = f02, h13: f12 ≫ f23 = f13, hf: f02 ≫ f23 = f, the 2‑cell component corresponding to the composite map along f02, f23, f is equal to a pasting involving the components of mapComp', the whiskering with F.map f01 on the left, the whiskering with F.map f23 on the right, and the associator. In other words, the coherence of mapComp' expresses that the hom part of the composite is obtained by pasting these 2-cells together with the associator.
Русский
Пусть F — псевдофунктор между бикатегориями B и C. Пусть имеем последовательность стрелок f01: X0 → X1, f12: X1 → X2, f23: X2 → X3, с композициями f02 = f01 ≫ f12, f13 = f12 ≫ f23, и f = f02 ≫ f23, а также равенства h02: f01 ≫ f12 = f02, h13: f12 ≫ f23 = f13, hf: f02 ≫ f23 = f. Тогда 2-одномерный компонент, связанный с композитом mapComp', для тройки (f02, f23, f), равен пастингу, включающему соответствующие компоненты mapComp', развёрнутый слева на F.map f01 и справа на F.map f23, а также ассоциатор.
LaTeX
$$$ (F.mapComp' f_{02} f_{23} f).hom = (F.mapComp' f_{01} f_{13} f).hom \\,\\gg \\\\ F.map f_{01} \\triangleleft (F.mapComp' f_{12} f_{23} f_{13} h_{13}).hom \\\\ gg (\\alpha_{F.map f_{01}, F.map f_{12}, F.map f_{23}})^{-1} \\\\ gg (F.mapComp' f_{01} f_{12} f_{02} h_{02})^{-1} \\triangleright F.map f_{23} $$$
Lean4
@[to_app (attr := reassoc)]
theorem mapComp'₀₂₃_hom (hf : f₀₂ ≫ f₂₃ = f) :
(F.mapComp' f₀₂ f₂₃ f).hom =
(F.mapComp' f₀₁ f₁₃ f).hom ≫
F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫ (α_ _ _ _).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ :=
by simp [← mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_assoc _ _ _ _ _ _ f h₀₂ h₁₃ hf]
