mathlib3

57d4b411 - feat(category_theory/limits): construct limits from products and equalizers (#1362)

feat(category_theory/limits): construct limits from products and equalizers (#1362) * providing minimal API for limits of special shapes * apis for special shapes * fintype instances * associators, unitors, braidings for binary product * map * instances * assoc lemma * coprod * fix import * names * adding some docs * updating tutorial on limits * minor * uniqueness of morphisms to terminal object * better treatment of has_terminal * various * not there yet * deleting a dumb file * remove constructions for a later PR * getting there * oops * of_nat_iso * feat(category_theory/limits/of_nat_isp) * progress on limits from products and equalizers * Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * use @[reassoc] * fixing after rename * use @[reassoc] * fix renaming * complete construction of limits from products and equalizers * cleanup * cleanup * name instance * whitespace * Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * use simpa