{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₂ ⟶ X₁} →
        {f₂ : X₃ ⟶ X₂} →
          {i₁ : Y₁ ⟶ X₁} →
            (t₁ : CategoryTheory.Limits.PullbackCone i₁ f₁) →
              {i₂ : t₁.pt ⟶ X₂} →
                CategoryTheory.Limits.PullbackCone i₂ f₂ →
                  i₂ = t₁.snd → CategoryTheory.Limits.PullbackCone i₁ (CategoryTheory.CategoryStruct.comp f₂ f₁)