∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type w₂} [inst_1 : CategoryTheory.Category.{w₁, w₂} C]
  [CategoryTheory.IsPreconnected J] {X Y : C}
  (α : (CategoryTheory.Functor.const J).obj X ⟶ (CategoryTheory.Functor.const J).obj Y) (j j' : J), α.app j = α.app j'