open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Subgroup
open import Algebra.Group.Ab.Sum
open import Algebra.Group.Ab

open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Abelian.Base
open import Cat.Prelude

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

open is-pre-abelian
open is-additive

open Terminal
open Product

The category of abelian groups🔗

The prototypal — representative, even — example of an $\mathbf{Ab}\text{-enriched}$, and an abelian category at that, is the category of abelian groups, $\mathbf{Ab}\text{.}$ For abstractly-nonsensical reasons, we could say $\mathbf{Ab}$ is $\mathbf{Ab}\text{-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 (∫hom (λ _ → lift tt) (record { pres-⋆ = λ x y i → lift tt }))
    λ x → trivial!

Ab-is-additive .has-prods A B .apex = A ⊕ B
Ab-is-additive .has-prods A B .π₁ = _
Ab-is-additive .has-prods A B .π₂ = _
Ab-is-additive .has-prods A B .has-is-product = Direct-sum-is-product