mathlib3
e3559335 - chore(category_theory/limits): remove unnecessary typeclass arguments (#4141)

Commit
5 years ago
chore(category_theory/limits): remove unnecessary typeclass arguments (#4141) Ongoing cleanup post #3995. Previously we couldn't construct things like `instance : has_kernel (0 : X \hom Y)`, because it wouldn't have agreed definitionally with more general instances. Now we can. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading