mathlib

465cf5ad - feat(category_theory/abelian): biproducts of projective objects are projective (#7319)

feat(category_theory/abelian): biproducts of projective objects are projective (#7319) Also all objects of `Type` are projective. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>