feat(category_theory/is_connected): constant functor is full (#8233)
feat(category_theory/is_connected): constant functor is full (#8233)

Shows the constant functor on a connected category is full.

Also golfs a later proof slightly.





leanprover-community/mathlib,leanprover-community/mathlib