mathlib documentation

category_theory.limits.shapes.functor_category

If D has finite (co)limits, so do the functor categories C ⥤ D. #

These are boiler-plate instances, in their own file as neither import otherwise needs the other.