Commit 2023-09-15 10:01 740d16ac
View on Github →feat: the quotient category is preadditive (#7049) It is shown in this PR that when an equivalence relation on morphisms in a preadditive category is compatible with the addition, then the quotient category is preadditive.