∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂)
  (X : CategoryTheory.GradedObject (I₁ × I₂) C) (d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂))
  (d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂'))
  (shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0)
  (shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0)
  (d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₁ i₁' i₁'' i₂) = 0)
  (d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₂ i₁ i₂' i₂'') = 0)
  (comm :
    ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂),
      CategoryTheory.CategoryStruct.comp (d₁ i₁ i₁' i₂) (d₂ i₁' i₂ i₂') =
        CategoryTheory.CategoryStruct.comp (d₂ i₁ i₂ i₂') (d₁ i₁ i₁' i₂'))
  (i₁ : I₁) (i₂ i₂' : I₂),
  ((HomologicalComplex₂.ofGradedObject c₁ c₂ X d₁ d₂ shape₁ shape₂ d₁_comp_d₁ d₂_comp_d₂ comm).X i₁).d i₂ i₂' =
    d₂ i₁ i₂ i₂'