∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : C},
  CategoryTheory.IsDetector G →
    ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
      (∀ (h : G ⟶ Y), ∃! h', CategoryTheory.CategoryStruct.comp h' f = h) → CategoryTheory.IsIso f