Commit 2020-06-29 13:48 a708f854

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.