∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : HomologicalComplex V c.symm} (f : X ⟶ Y),
  (HomologicalComplex.unopInverse V c).map f = Quiver.Hom.op { f := fun i => (f.f i).op, comm' := ⋯ }