English
Under the same hypotheses as above, the inverse of the 2‑cell component mapComp' satisfies a dual pasting formula: the inv of mapComp' f02 f23 f equals the left whiskered inverse of mapComp' f01 f12 f02 h02, whiskered on the right by f23, followed by the associator’s hom, and then whiskered on the left by F.map f01 with the inverse of mapComp' f12 f23 f13 h13, and finally whiskered on the right with the inverse of mapComp' f01 f13 f.
Русский
При тех же предпосылках обратная часть 2-ячейки mapComp' удовлетворяет двойной пастингу:Inv mapComp' f_{02} f_{23} f равен левой штриховке (обратной) mapComp' f_{01} f_{12} f_{02} h_{02}, затем развёрнутая ассоциаторная часть, далее левая штриховка F.map f_{01} и обратная часть mapComp' f_{12} f_{23} f_{13} h_{13}, и, наконец, правая штриховка с обратной частью mapComp' f_{01} f_{13} f.
LaTeX
$$$ (F.mapComp' f_{02} f_{23} f).inv = (F.mapComp' f_{01} f_{12} f_{02} h_{02}).hom \\triangleright F.map f_{23} \\; \\gg \\; (\\alpha_{\\cdot})^{\\mathrm{hom}} \\; \\gg \\; F.map f_{01} \\triangleleft (F.mapComp' f_{12} f_{23} f_{13} h_{13}).inv \\; \\gg \\; (F.mapComp' f_{01} f_{13} f).inv $$
Lean4
@[to_app (attr := reassoc)]
theorem mapComp'₀₂₃_inv (hf : f₀₂ ≫ f₂₃ = f) :
(F.mapComp' f₀₂ f₂₃ f).inv =
(F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫
(α_ _ _ _).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f).inv :=
by
rw [← cancel_epi (F.mapComp' f₀₂ f₂₃ f).hom, Iso.hom_inv_id]
simp [mapComp'₀₂₃_hom _ _ _ _ _ _ f h₀₂ h₁₃ hf]
