precomposeObjTransformObjSquare — Mathlib

Lean4
/-- The canonical compatibility square between (the object components of)
`precompose` and `transform`.
This is a "naturality square" if we think as `transform _|>.obj _` as the
(app component of the) map component of a pseudofunctor from the bicategory of
categorical cospans with value in pseudofunctors
(its value on the categorical cospan `F, G` being the pseudofunctor
`precompose F G|>.obj _`). -/
@[simps!]
instance precomposeObjTransformObjSquare {X : Type u₇} {Y : Type u₈} [Category.{v₇} X] [Category.{v₈} Y]
    (ψ : CatCospanTransform F G F₁ G₁) (U : X ⥤ Y) :
    CatCommSq (precompose F G |>.obj U) (transform Y |>.obj ψ) (transform X |>.obj ψ) (precompose F₁ G₁ |>.obj U) where
  iso :=
    NatIso.ofComponents fun _ =>
      CategoricalPullback.mkIso (Functor.associator _ _ _)
        (Functor.associator _ _ _)
          -- Compare the next 3 lemmas with the components of a strong natural transform
          -- of pseudofunctors
Похожие утверждения