module Cat.Abelian.Instances.Ab {} where

The category of abelian groups🔗

The prototypal — representative, even — example of an , and an abelian category at that, is the category of abelian groups, For abstractly-nonsensical reasons, we could say is 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