1: \begin{abstract}

2:   We show that categories of modules over a ring in Homotopy Type Theory (HoTT) satisfy the internal versions of the AB axioms from homological algebra.

3:   The main subtlety lies in proving AB4, which is that coproducts indexed by arbitrary sets are left-exact.

4:   To prove this, we replace a set with its strict category of (ordered) finite sub-multisets.

5:   From showing that the latter is filtered, we deduce left-exactness of the coproduct.

6:   More generally, we show that exactness of filtered colimits (AB5) implies AB4 for any abelian category in HoTT.

7:   Our approach is heavily inspired by Roswitha Harting's construction of the {\em internal coproduct} of abelian groups in an elementary topos with a natural numbers object~\cite{Har82}.

8: 

9:   To state the AB axioms we define and study filtered (and sifted) precategories in HoTT.

10:   A key result needed is that filtered colimits commute with finite limits of sets.

11:   This is a familiar classical result, but has not previously been checked in our setting.

12: 

13:   Finally, we interpret our most central results into an \(\infty\)-topos \( \XX \).

14:   Given a ring \( R \) in \( \XX \), we show that the internal category of \(R\)-modules in \( \XX \) represents the presheaf which sends an object \( X \in \XX \) to the category of \( (X{\times}R) \)-modules over \( X \).

15:   In general, our results yield a product-preserving left adjoint to base change of modules over \( X \).

16:   When \( X \) is \(0\)-truncated, this left adjoint is the internal coproduct.

17:   By an internalisation procedure, we deduce left-exactness of the internal coproduct as an ordinary functor from its internal left-exactness coming from HoTT.

18: \end{abstract}

19: