∀ {C : Type u_6} [inst : CategoryTheory.Category.{u_5, u_6} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{u_3, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{u_4, u_2} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {y₁ y₂ : CategoryTheory.ThinSkeleton D} (a : C),
  Subsingleton
    ((y₁ ⟶ y₂) → (CategoryTheory.ThinSkeleton.map₂ObjMap F ⟦a⟧ y₁ ⟶ CategoryTheory.ThinSkeleton.map₂ObjMap F ⟦a⟧ y₂))