{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J C) →
          [inst_2 : CategoryTheory.Limits.HasTerminal J] →
            [inst_3 : ∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)] →
              CategoryTheory.Limits.limit F ≅ F.obj (⊤_ J)