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

open import Cat.Functor.Adjoint.Continuous
open import Cat.Diagram.Equaliser.Kernel
open import Cat.Functor.FullSubcategory
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Functor.Adjoint
open import Cat.Abelian.Base
open import Cat.Prelude

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

open is-additive.Coequaliser
open is-additive.Terminal
open is-pre-abelian
open Ab-category
open is-additive
open make-group

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