mathlib3

afe51c76 - feat(category_theory/limits): special shapes (#1339)

feat(category_theory/limits): special shapes (#1339) * 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 * use @[reassoc] * Update src/category_theory/limits/shapes/finite_products.lean Co-Authored-By: Johan Commelin <johan@commelin.net> * improving the colimits tutorial * minor * notation for `prod_obj` and `sigma_obj`. * reverting to `condition` * implicit arguments * more implicit arguments * minor * notational for initial and terminal objects * various * fix notation priorities * remove unused case bash tactic * fix whitespace * comment * notations