Commit 2020-09-14 06:53 e3559335

View on Github →

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.

Estimated changes

Modified src/category_theory/limits/shapes/equalizers.lean

modified def category_theory.limits.coequalizer.iso_target_of_self

modified theorem category_theory.limits.coequalizer.iso_target_of_self_hom

modified theorem category_theory.limits.coequalizer.iso_target_of_self_inv

modified def category_theory.limits.equalizer.iso_source_of_self

modified theorem category_theory.limits.equalizer.iso_source_of_self_hom

modified theorem category_theory.limits.equalizer.iso_source_of_self_inv

Modified src/category_theory/limits/shapes/kernels.lean

modified def category_theory.limits.cokernel.π_of_zero

modified def category_theory.limits.cokernel_zero_iso_target

modified theorem category_theory.limits.cokernel_zero_iso_target_hom

modified theorem category_theory.limits.cokernel_zero_iso_target_inv

modified def category_theory.limits.kernel.ι_of_zero

modified def category_theory.limits.kernel_zero_iso_source

modified theorem category_theory.limits.kernel_zero_iso_source_hom

modified theorem category_theory.limits.kernel_zero_iso_source_inv