{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {motive : CategoryTheory.Classifier C → Sort u_1} →
      ((Ω₀ Ω : C) →
          (truth : Ω₀ ⟶ Ω) →
            (mono_truth : CategoryTheory.Mono truth) →
              (χ₀ : (U : C) → U ⟶ Ω₀) →
                (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω) →
                  (isPullback :
                      ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m],
                        CategoryTheory.IsPullback m (χ₀ U) (χ m) truth) →
                    (uniq :
                        ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀} {χ' : X ⟶ Ω},
                          CategoryTheory.IsPullback m χ₀' χ' truth → χ' = χ m) →
                      motive
                        { Ω₀ := Ω₀, Ω := Ω, truth := truth, mono_truth := mono_truth, χ₀ := χ₀, χ := χ,
                          isPullback := isPullback, uniq := uniq }) →
        (t : CategoryTheory.Classifier C) → motive t