Commit 2021-04-20 07:56 5e188d2f

feat(category_theory/abelian): definition of projective object (#7108) This is extracted from @TwoFX's projective branch, with some slight tweaks (make things Prop valued classes), and documentation. This is just the definition of projective and enough_projectives, with no attempt to construct projective resolutions. I want this in place because constructing projective resolutions will hopefully be a good test of experiments with chain complexes.