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
1. additional theorems providing `total`, when `preadditive C` is available
2. 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.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
