Characterization of connected categories using initial/final functors

A category C is connected iff the constant functor C ⥤ Discrete PUnit is final (or initial).

We deduce that the projection C × D ⥤ C is final (or initial) if D is connected.

theorem CategoryTheory.isConnected_iff_final_of_unique {C : Type u} [Category.{v, u} C] {T : Type w} [Unique T] (F : Functor C (Discrete T)) : IsConnected C ↔ F.Final

theorem CategoryTheory.isConnected_iff_initial_of_unique {C : Type u} [Category.{v, u} C] {T : Type w} [Unique T] (F : Functor C (Discrete T)) : IsConnected C ↔ F.Initial

instance CategoryTheory.instFinalDiscreteOfIsConnected {C : Type u} [Category.{v, u} C] {T : Type w} [Unique T] (F : Functor C (Discrete T)) [IsConnected C] : F.Final

instance CategoryTheory.instInitialDiscreteOfIsConnected {C : Type u} [Category.{v, u} C] {T : Type w} [Unique T] (F : Functor C (Discrete T)) [IsConnected C] : F.Initial

instance CategoryTheory.final_fst {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [IsConnected D] : (Prod.fst C D).Final

instance CategoryTheory.final_snd {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [IsConnected C] : (Prod.snd C D).Final

instance CategoryTheory.initial_fst {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [IsConnected D] : (Prod.fst C D).Initial

instance CategoryTheory.initial_snd {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [IsConnected C] : (Prod.snd C D).Initial