module Cat.Abelian.Instances.Ab {β} where

# The category of abelian groupsπ

The prototypal β representative, even β example of an $\mathbf{Ab}$-enriched,
and an abelian
category at that, is the category of abelian groups,
$\mathbf{Ab}$.
For abstractly-nonsensical reasons, we could say
$\mathbf{Ab}$
is
$\mathbf{Ab}$-enriched
by virtue of being monoidal closed, but we have a concrete construction
at hand: `Ab-ab-category`

Let us show it is additive. The terminal group is given by the terminal set, equipped with its unique group structure, and we have already computed products β they are given by direct sums.

Ab-is-additive : is-additive (Ab β) Ab-is-additive .has-ab = Ab-ab-category Ab-is-additive .has-terminal .top = from-commutative-group (Zero-group {β}) (Ξ» x y β refl) Ab-is-additive .has-terminal .hasβ€ x = contr (total-hom (Ξ» _ β lift tt) (record { pres-β = Ξ» x y i β lift tt })) Ξ» x β Homomorphism-path Ξ» _ β refl Ab-is-additive .has-prods A B .Product.apex = A β B Ab-is-additive .has-prods A B .Product.Οβ = _ Ab-is-additive .has-prods A B .Product.Οβ = _ Ab-is-additive .has-prods A B .Product.has-is-product = Direct-sum-is-product