bifunctorComp₂₃ — Mathlib

Lean4
/-- The construction `bifunctorComp₂₃` of a trifunctor by composition of bifunctors
is compatible with localization. -/
noncomputable def bifunctorComp₂₃ :
    Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ ((Functor.postcompose₃.obj L).obj (bifunctorComp₂₃ F G₂₃)) (bifunctorComp₂₃ F' G₂₃')
    where
  iso :=
    ((whiskeringLeft _ _ _).obj L₁).mapIso
        ((bifunctorComp₂₃Functor.obj F').mapIso
          (Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight _ _ _).obj L₂₃) G₂₃')) ≪≫
      (bifunctorComp₂₃Functor.mapIso (Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight _ _ _).obj L) F')).app G₂₃
Похожие утверждения