∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {Ω₀ Ω : 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}
  {Ω₀_1 Ω_1 : C} {truth_1 : Ω₀_1 ⟶ Ω_1} {mono_truth_1 : CategoryTheory.Mono truth_1} {χ₀_1 : (U : C) → U ⟶ Ω₀_1}
  {χ_1 : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω_1}
  {isPullback_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀_1 U) (χ_1 m) truth_1}
  {uniq_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀_1} {χ' : X ⟶ Ω_1},
      CategoryTheory.IsPullback m χ₀' χ' truth_1 → χ' = χ_1 m},
  { Ω₀ := Ω₀, Ω := Ω, truth := truth, mono_truth := mono_truth, χ₀ := χ₀, χ := χ, isPullback := isPullback,
        uniq := uniq } =
      { Ω₀ := Ω₀_1, Ω := Ω_1, truth := truth_1, mono_truth := mono_truth_1, χ₀ := χ₀_1, χ := χ_1,
        isPullback := isPullback_1, uniq := uniq_1 } →
    Ω₀ = Ω₀_1 ∧ Ω = Ω_1 ∧ truth ≍ truth_1 ∧ χ₀ ≍ χ₀_1 ∧ χ ≍ χ_1