mathlib

b4e6313a - feat(category_theory): subsingleton (has_zero_morphisms) (#2180)

feat(category_theory): subsingleton (has_zero_morphisms) (#2180) * feat(category_theory): subsingleton (has_zero_morphisms) * fix * Update src/category_theory/limits/shapes/zero.lean Co-Authored-By: Markus Himmel <markus@himmel-villmar.de> * Update src/category_theory/limits/shapes/zero.lean Co-Authored-By: Markus Himmel <markus@himmel-villmar.de> * non-terminal simp * add warning message * Update src/category_theory/discrete_category.lean Co-Authored-By: Markus Himmel <markus@himmel-villmar.de> * Apply suggestions from code review Co-authored-by: Markus Himmel <markus@himmel-villmar.de> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>