∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (obj₁ obj₂ obj₃ : C)
  (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁)
  (obj₁_1 obj₂_1 obj₃_1 : C) (mor₁_1 : obj₁_1 ⟶ obj₂_1) (mor₂_1 : obj₂_1 ⟶ obj₃_1)
  (mor₃_1 : obj₃_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁_1),
  ({ obj₁ := obj₁, obj₂ := obj₂, obj₃ := obj₃, mor₁ := mor₁, mor₂ := mor₂, mor₃ := mor₃ } =
      { obj₁ := obj₁_1, obj₂ := obj₂_1, obj₃ := obj₃_1, mor₁ := mor₁_1, mor₂ := mor₂_1, mor₃ := mor₃_1 }) =
    (obj₁ = obj₁_1 ∧ obj₂ = obj₂_1 ∧ obj₃ = obj₃_1 ∧ mor₁ ≍ mor₁_1 ∧ mor₂ ≍ mor₂_1 ∧ mor₃ ≍ mor₃_1)