∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X Y : A) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (ι.map (Λ.F.map f)) (Λ.π.app Y) = CategoryTheory.CategoryStruct.comp (Λ.π.app X) f