feat(category_theory/limits/concrete): simp lemmas (#3973)
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element.
This isn't exhaustive; just the things I've wanted recently.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
