Add semi-additive categories infrastructure

Extracting SemiAdditive.v from additive categories work per PR HoTT#2304 review.

**Provides:**
- `SemiAdditiveCategory`: Class with just cat, zero object, and biproducts
- Derives `IsCommutativeMonoid` structure on morphisms using biproducts
- Addition defined as: f + g = ∇ ∘ (f ⊕ g) ∘ Δ  
- Proves identity laws, commutativity, associativity from biproduct axioms
- Bilinearity of composition (distributivity)

**Note:** The file is almost 1000 lines), especially the associativity proof. This was the only way I could get it to work - would very much appreciate help simplifying and identifying which helper lemmas can be removed. The associativity proof in particular requires many intermediate lemmas about how biproducts interact. It took me an entire week of 16 hour days to get here, but I assume there is a much more elegant method.

Addresses review feedback from HoTT#2304. Next step is to update AdditiveCategories.v to build on this, adding only the inverse axiom.

Author: CharlesCNorton