feat(category_theory/limits): morphism to terminal is split mono (#8084)
feat(category_theory/limits): morphism to terminal is split mono (#8084)

A generalisation of existing results: we already have an instance `split_mono` to `mono` so this is strictly more general.





leanprover-community/mathlib,leanprover-community/mathlib