# Commit 2020-06-29 13:48 a708f854

View on Github →feat(category/limits/shapes): fix biproducts (#3175)
This is a second attempt at #3102.
Previously the definition of a (binary) biproduct in a category with zero morphisms (but not necessarily) preadditive was just wrong.
The definition for a "bicone" was just something that was simultaneously a cone and a cocone, with the same cone points. It was a "biproduct bicone" if the cone was a limit cone and the cocone was a colimit cocone. However, this definition was not particularly useful. In particular, there was no way to prove that the two different `map`

constructions providing a morphism `W ⊞ X ⟶ Y ⊞ Z`

(i.e. by treating the biproducts either as cones, or as cocones) were actually equal. Blech.
So, I've added the axioms `inl ≫ fst = 𝟙 P`

, `inl ≫ snd = 0`

, `inr ≫ fst = 0`

, and `inr ≫ snd = 𝟙 Q`

to `bicone P Q`

. (Note these only require the exist of zero morphisms, not preadditivity.)
Now the two map constructions are equal.
I've then entirely removed the `has_preadditive_biproduct`

typeclass. Instead we have

- additional theorems providing
`total`

, when`preadditive C`

is available - alternative constructors for
`has_biproduct`

that use`total`

rather than`is_limit`

and`is_colimit`

. This PR also introduces some abbreviations along the lines of`abbreviation has_binary_product (X Y : C) := has_limit (pair X Y)`

, just to improve readability.