transformObjPrecomposeObjSquare — Mathlib

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