Commit 2021-03-16 10:12 57de126a

View on Github →

refactor(category_theory/limits): use auto_param (#6696) Add an auto_param, making it slightly more convenient when build limits of particular shapes first, then all limits.

Estimated changes

Modified src/category_theory/limits/constructions/over/default.lean

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/limits.lean

Modified src/category_theory/limits/opposites.lean

modified theorem category_theory.limits.has_colimits_op_of_has_limits

modified theorem category_theory.limits.has_limits_op_of_has_colimits

Modified src/category_theory/limits/over.lean

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