{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (Ω₀ : C) →
      (t : CategoryTheory.Limits.IsTerminal Ω₀) →
        (Ω : C) →
          (truth : Ω₀ ⟶ Ω) →
            (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) →
              (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m],
                  CategoryTheory.IsPullback m (t.from U) (χ m) truth) →
                (∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] (χ' : X ⟶ Ω),
                    CategoryTheory.IsPullback m (t.from U) χ' truth → χ' = χ m) →
                  CategoryTheory.Subobject.Classifier C