English
The square transformPrecomposeObjSquare is compatible with compositions, i.e., the map of ψ.comp ψ' relates to the composition of the corresponding transforms with associators and whiskers in a way that matches the expected coherence in CatCommSqOver.
Русский
Квадрат transformPrecomposeObjSquare сохраняет композиции, то есть отображение ψ.comp ψ' связано с композицией соответствующих преобразований с участием ассоциаторов и whisker-операций так, чтобы согласовываться с когерентностью в CatCommSqOver.
LaTeX
$$$ (\\text{transformObjPrecomposeObjSquare } U (ψ.{\\}\\cdot ψ')).hom \\\\;\\circ \\\\; (\\, ... ) = \\\\; \\mathrm{comp} \\ (\\text{whiskerRight } η (\\text{transformX} ψ)).hom \\cdot (\\text{...})$$$
Lean4
/-- The square `transformObjPrecomposeObjSquare` is itself natural. -/
theorem transformObjPrecomposeObjSquare_iso_hom_naturality₂ {X : Type u₇} {Y : Type u₈} [Category.{v₇} X]
[Category.{v₈} Y] (U : X ⥤ Y) {ψ ψ' : CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') :
whiskerRight (transform Y |>.map η) (precompose F₁ G₁ |>.obj U) ≫
(CatCommSq.iso _ (precompose F G |>.obj U) _ (transform X |>.obj ψ')).hom =
(CatCommSq.iso _ (precompose F G |>.obj U) _ (transform X |>.obj ψ)).hom ≫
whiskerLeft (precompose F G |>.obj U) (transform X |>.map η) :=
by cat_disch
