{J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} →
      {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} →
        {e : J} →
          D.W (CategoryTheory.CategoryStruct.id e) →
            (lift : {j : J} → D.P j → (j ⟶ e)) →
              (∀ {j : J} (hj : D.P j), D.W (lift hj)) →
                (∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ) →
                  (∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯) →
                    D.IsTerminal e