bifunctorComp₁₂FunctorObj — Mathlib

Lean4

/-- Auxiliary definition for `bifunctorComp₁₂Functor`. -/
@[simps]
def bifunctorComp₁₂FunctorObj (F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂) : (C₁₂ ⥤ C₃ ⥤ C₄) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
    where
  obj G := bifunctorComp₁₂ F₁₂ G
  map {G G'}
    φ :=
    { app
        X₁ :=
        { app X₂ := { app X₃ := (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃ }
          naturality := fun X₂ Y₂ f ↦ by
            ext X₃
            dsimp
            simp only [← NatTrans.comp_app, NatTrans.naturality] }
      naturality X₁ Y₁
        f := by
        ext X₂ X₃
        dsimp
        simp only [← NatTrans.comp_app, NatTrans.naturality] }

Похожие утверждения