English
Given ψ : CatCospanTransform F G F₁ G₁ and U,V : X ⥤ Y, the naturality statement expresses that the precomposition square respects compositions of functors, i.e., the transform of ψ.comp ψ' equals the appropriate composite of transforms and whiskers, illustrating coherence with composition in CatCommSqOver.
Русский
Дано ψ : CatCospanTransform F G F₁ G₁ и U,V : X ⥤ Y; естественность выражает, что квадрат предкомпонования сохраняет композиции, т.е. преобразование ψ.comp ψ' равняется соответствующей композиции преобразований и whisker-операций, демонстрируя когерентность с композициями в CatCommSqOver.
LaTeX
$$$ \\text{(precomposeObjTransformObjSquare } ψ U).hom = \\text{(transformObjPrecomposeObjSquare } ψ U).iso \\; \\circ \\\\; \\hspace{-2pt} ((\\text{transform Y}|>.obj ψ).whiskerLeft ( (\\text{precompose F G}.obj U) \\ )).hom$$$
Lean4
/-- The square `precomposeObjTransformOBjSquare` respects identities. -/
theorem precomposeObjTransformObjSquare_iso_hom_id (ψ : CatCospanTransform F G F₁ G₁) (X : Type u₇) [Category.{v₇} X] :
(CatCommSq.iso (precompose F G |>.obj <| 𝟭 X) (transform X |>.obj ψ) (transform X |>.obj ψ)
(precompose F₁ G₁ |>.obj <| 𝟭 X)).hom ≫
whiskerLeft (transform X |>.obj ψ) (precomposeObjId F₁ G₁ X).hom =
whiskerRight (precomposeObjId F G X).hom (transform X |>.obj ψ) ≫
(Functor.leftUnitor _).hom ≫ (Functor.rightUnitor _).inv :=
by cat_disch
