∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_3} (c : ComplexShape ι) (i : ι) [inst_3 : DecidableEq ι]
  (hi : ∀ (j : ι), ¬c.Rel i j) (X : C) {Y Y' : HomologicalComplex C c} (g : Y ⟶ Y')
  (f : (HomologicalComplex.single C c i).obj X ⟶ Y),
  { toFun := fun g => CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv (g.f i),
        invFun := fun f => HomologicalComplex.mkHomFromSingle f ⋯, left_inv := ⋯, right_inv := ⋯ }
      (CategoryTheory.CategoryStruct.comp f g) =
    ((HomologicalComplex.eval C c i).comp (CategoryTheory.coyoneda.obj (Opposite.op X))).map g
      ({ toFun := fun g => CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv (g.f i),
          invFun := fun f => HomologicalComplex.mkHomFromSingle f ⋯, left_inv := ⋯, right_inv := ⋯ }
        f)