∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (cc : CategoryTheory.Limits.CokernelCofork S.f) (hcc : CategoryTheory.Limits.IsColimit cc),
  (hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt