mathlib

d201a182 - refactor(algebra/homology/homotopy): avoid needing has_zero_object (#7621)

refactor(algebra/homology/homotopy): avoid needing has_zero_object (#7621) A refactor of the definition of `homotopy`, so we don't need `has_zero_object`. Co-authored-by: Adam Topaz github@adamtopaz.com Co-authored-by: Adam Topaz <github@adamtopaz.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>