English
For a LaxFunctor F, a relation hf: f01 ≫ f13 = f, the equality relates the left whiskering of mapComp' with a rightward whisker, giving a coherence between map and whiskering in the left and right directions.
Русский
Для LaxFunctor F и hf: f01 ≫ f13 = f, имеется равенство, связывающее левую штриховку mapComp' с правой штриховкой, задающее когеренцию между отображением и штрихованием слева и справа.
LaTeX
$$$ F.map f_{01} \\triangleleft F.mapComp' f_{12} f_{23} f_{13} h_{13} ≫ F.mapComp' f_{01} f_{13} f hf = (\\alpha_{...})^{ -1} ≫ F.map f_{01} \\triangleleft (F.mapComp' f_{12} f_{23} f_{13} h_{13}).hom ≫ F.mapComp' f_{01} f_{13} f hf $$$
Lean4
@[reassoc]
theorem whiskerLeft_mapComp'_comp_mapComp' (hf : f₀₁ ≫ f₁₃ = f) :
F.map f₀₁ ◁ F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃ ≫ F.mapComp' f₀₁ f₁₃ f hf =
(α_ _ _ _).inv ≫ F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂ ▷ F.map f₂₃ ≫ F.mapComp' f₀₂ f₂₃ f :=
by
subst hf h₀₂ h₁₃
have := F.map₂_associator f₀₁ f₁₂ f₂₃
simp only [Strict.associator_eqToIso, eqToIso.hom] at this
simp [LaxFunctor.mapComp', this]
