map₂CompMap₂Iso — Mathlib

Lean4

/-- The composition of two applications of `map₂` is naturally isomorphic to a single such one. -/
def map₂CompMap₂Iso {C' : Type u₆} [Category.{v₆} C'] {D' : Type u₅} [Category.{v₅} D'] {L'' : D'} {R'' : C' ⥤ D'}
    {F' : C' ⥤ C} {G' : D' ⥤ D} (α' : L ⟶ G'.obj L'') (β' : R'' ⋙ G' ⟶ F' ⋙ R) :
    map₂ α' β' ⋙ map₂ α β ≅
      map₂ (α ≫ G.map α')
        ((Functor.associator _ _ _).inv ≫
          Functor.whiskerRight β' _ ≫
            (Functor.associator _ _ _).hom ≫ Functor.whiskerLeft _ β ≫ (Functor.associator _ _ _).inv) :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _))

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