{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            HomologicalComplex.restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ≅ K