Commit 2020-05-13 10:27 506a71f9

View on Github →

feat(category_theory): preadditive categories (#2663) As discussed, here is the pedestrian definition of preadditive categories. Hopefully, it is not here to stay, but it will allow me to start PRing abelian categories.

Estimated changes