English
Coherence of the associator under the CatCommSqOver transform: the image of the associator equals a long composite built from associators, whiskers, and transformObjComp/conjugates, ensuring coherence of the construction.
Русский
Когерентность ассоциатора под преобразованием CatCommSqOver: образ ассоциатора равен длинной композиции из ассоциаторов, взвешиваний и transformObjComp, обеспечивая когерентность конструкции.
LaTeX
$$$ (transform X).map (α_ ψ φ τ).hom = (transformObjComp X (ψ.comp φ) τ).hom \circ whiskerRight (transformObjComp X ψ φ).hom (transform X |>.obj τ) \circ ((transform X |>.obj ψ).associator (transform X |>.obj φ) (transform X |>.obj τ)).hom \circ whiskerLeft (transform X |>.obj ψ) (transformObjComp X φ τ).inv \circ (transformObjComp X ψ (φ.comp τ)).inv $$$
Lean4
theorem transform_map_whiskerLeft (X : Type u₇) [Category.{v₇} X] (ψ : CatCospanTransform F G F₁ G₁)
{φ φ' : CatCospanTransform F₁ G₁ F₂ G₂} (α : φ ⟶ φ') :
(transform X).map (ψ ◁ α) =
(transformObjComp X ψ φ).hom ≫
whiskerLeft (transform X |>.obj ψ) (transform X |>.map α) ≫ (transformObjComp X ψ φ').inv :=
by cat_disch
