∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.CategoryStruct.comp (𝒞₂.hom 𝒞₁) (𝒞₁.hom 𝒞₂) = CategoryTheory.CategoryStruct.id 𝒞₂.Ω