{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.HasShift C ℤ} →
      {P : Sort u_1} →
        {obj₁ obj₂ obj₃ : C} →
          {mor₁ : obj₁ ⟶ obj₂} →
            {mor₂ : obj₂ ⟶ obj₃} →
              {mor₃ : obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁} →
                {obj₁' obj₂' obj₃' : C} →
                  {mor₁' : obj₁' ⟶ obj₂'} →
                    {mor₂' : obj₂' ⟶ obj₃'} →
                      {mor₃' : obj₃' ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁'} →
                        { obj₁ := obj₁, obj₂ := obj₂, obj₃ := obj₃, mor₁ := mor₁, mor₂ := mor₂, mor₃ := mor₃ } =
                            { obj₁ := obj₁', obj₂ := obj₂', obj₃ := obj₃', mor₁ := mor₁', mor₂ := mor₂',
                              mor₃ := mor₃' } →
                          (obj₁ ≍ obj₁' →
                              obj₂ ≍ obj₂' → obj₃ ≍ obj₃' → mor₁ ≍ mor₁' → mor₂ ≍ mor₂' → mor₃ ≍ mor₃' → P) →
                            P