∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] (a b c : CategoryTheory.ThinSkeleton C),
  Quotient.lift₂ (fun X Y => Nonempty (X ⟶ Y)) ⋯ a b →
    Quotient.lift₂ (fun X Y => Nonempty (X ⟶ Y)) ⋯ b c → Quotient.lift₂ (fun X Y => Nonempty (X ⟶ Y)) ⋯ a c