diff --git a/theories/Categories/Additive/Additive.v b/theories/Categories/Additive/Additive.v
new file mode 100644
index 00000000000..398f14027cf
--- /dev/null
+++ b/theories/Categories/Additive/Additive.v
@@ -0,0 +1,117 @@
+(** * Additive categories
+
+    Semi-additive categories in which morphism addition admits inverses,
+    so that hom-sets are abelian groups and composition is bilinear. *)
+
+From HoTT Require Import Basics.Overture Basics.Tactics.
+From HoTT.Classes.interfaces Require Import canonical_names abstract_algebra.
+From HoTT.Categories Require Import Category.Core Functor.Core.
+From HoTT.Categories.Functor Require Import Identity Composition.Core.
+From HoTT.Categories.Additive Require Import ZeroObjects SemiAdditive.
+From HoTT.Algebra.AbGroups Require Import AbelianGroup.
+
+Local Open Scope morphism_scope.
+
+(** This lets us use "+", "-" and "0" notation for the commutative monoid
+    structure on hom-sets defined in SemiAdditive.v. *)
+Local Open Scope mc_add_scope.
+
+(** ** Definition of additive category
+
+    The commutative monoid structure on hom-sets of a semi-additive category
+    is canonical, so an additive category only needs to assume that each
+    morphism has an additive inverse. *)
+
+Class AdditiveCategory := {
+  additive_semiadditive :: SemiAdditiveCategory;
+
+  additive_inverse :: forall (X Y : object additive_semiadditive),
+    Inverse (morphism additive_semiadditive X Y);
+
+  additive_inverse_l : forall {X Y : object additive_semiadditive}
+    (f : morphism additive_semiadditive X Y),
+    (- f) + f = 0;
+}.
+
+Coercion additive_semiadditive : AdditiveCategory >-> SemiAdditiveCategory.
+
+(** ** Hom-sets are abelian groups *)
+
+Section HomAbGroup.
+  Context {A : AdditiveCategory} (X Y : object A).
+
+  (** The bundled abelian group of morphisms from [X] to [Y]. *)
+  Definition abgroup_hom : AbGroup
+    := Build_AbGroup' (morphism A X Y) _ _ _ additive_inverse_l.
+
+  #[export] Instance isabgroup_morphisms : IsAbGroup (morphism A X Y)
+    := @isabgroup_abgroup abgroup_hom.
+
+End HomAbGroup.
+
+(** ** Negation and composition *)
+
+(** A left additive inverse equals the negation. *)
+Definition hom_moveL_1V {A : AdditiveCategory} {X Y : object A}
+  {f g : morphism A X Y} (H : g + f = 0)
+  : g = - f
+  := grp_moveL_1V (G:=abgroup_hom X Y) H.
+
+(** Negation is compatible with precomposition. *)
+Definition inverse_precompose {A : AdditiveCategory} {X Y W : object A}
+  (f : morphism A X Y) (a : morphism A W X)
+  : (- f) o a = - (f o a).
+Proof.
+  apply hom_moveL_1V.
+  lhs_V napply addition_precompose.
+  lhs napply (ap (fun g => g o a) (additive_inverse_l f)).
+  napply zero_morphism_left.
+Qed.
+
+(** Negation is compatible with postcomposition. *)
+Definition inverse_postcompose {A : AdditiveCategory} {X Y W : object A}
+  (a : morphism A Y W) (f : morphism A X Y)
+  : a o (- f) = - (a o f).
+Proof.
+  apply hom_moveL_1V.
+  lhs_V napply addition_postcompose.
+  lhs napply (ap (fun g => a o g) (additive_inverse_l f)).
+  napply zero_morphism_right.
+Qed.
+
+(** ** Additive functors
+
+    A functor between additive categories is additive when its action on
+    each hom-set is a monoid homomorphism for the canonical addition.
+    Such functors automatically preserve zero morphisms and negation. *)
+
+Record AdditiveFunctor (A B : AdditiveCategory) := {
+  addfunctor :> Functor A B;
+
+  ismonoidpreserving_addfunctor :: forall (X Y : object A),
+    IsMonoidPreserving (@morphism_of _ _ addfunctor X Y);
+}.
+
+Arguments addfunctor {A B} F : rename.
+Arguments ismonoidpreserving_addfunctor {A B} F X Y : rename.
+
+(** The identity functor is additive. *)
+Definition id_additive_functor (A : AdditiveCategory)
+  : AdditiveFunctor A A.
+Proof.
+  snapply Build_AdditiveFunctor.
+  - exact 1%functor.
+  - intros X Y.
+    rapply id_monoid_morphism.
+Defined.
+
+(** Additive functors compose. *)
+Definition compose_additive_functors {A B C : AdditiveCategory}
+  (G : AdditiveFunctor B C) (F : AdditiveFunctor A B)
+  : AdditiveFunctor A C.
+Proof.
+  snapply Build_AdditiveFunctor.
+  - exact (G o F)%functor.
+  - intros X Y.
+    rapply compose_monoid_morphism.
+Defined.