{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          (t : CategoryTheory.Limits.PullbackCone f g) →
            (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt ⟶ t.pt) →
              (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                  CategoryTheory.CategoryStruct.comp (lift s) t.fst = s.fst) →
                (∀ (s : CategoryTheory.Limits.PullbackCone f g),
                    CategoryTheory.CategoryStruct.comp (lift s) t.snd = s.snd) →
                  (∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ t.pt),
                      (∀ (j : CategoryTheory.Limits.WalkingCospan),
                          CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) →
                        m = lift s) →
                    CategoryTheory.Limits.IsLimit t