diff --git a/theories/Categories/Additive/ZeroObjects.v b/theories/Categories/Additive/ZeroObjects.v
new file mode 100644
index 0000000000..a7bc3f571c
--- /dev/null
+++ b/theories/Categories/Additive/ZeroObjects.v
@@ -0,0 +1,88 @@
+(** * Zero objects in categories
+
+    Zero objects (both initial and terminal) and zero morphisms, foundational
+    concepts for additive and stable category theory.
+*)
+
+From HoTT Require Import Basics Types.
+From HoTT.Categories Require Import Category Functor NaturalTransformation.
+From HoTT.Categories Require Import InitialTerminalCategory.
+
+(** * Zero objects
+    
+    A zero object in a category is an object that is both initial and terminal.
+    Such objects play a fundamental role in additive and abelian categories,
+    where they enable the definition of zero morphisms and kernels.
+*)
+
+Class ZeroObject (C : PreCategory) := {
+  zero : object C;
+  is_initial :: IsInitialObject C zero;
+  is_terminal :: IsTerminalObject C zero
+}.
+
+Coercion zero : ZeroObject >-> object.
+
+Arguments zero {C} z : rename.
+Arguments is_initial {C} z : rename.
+Arguments is_terminal {C} z : rename.
+
+Instance initialobject_zeroobject {C : PreCategory} (Z : ZeroObject C)
+  : InitialObject C
+  := {| object_initial := zero Z; isinitial_object_initial := _ |}.
+
+Instance terminalobject_zeroobject {C : PreCategory} (Z : ZeroObject C)
+  : TerminalObject C
+  := {| object_terminal := zero Z; isterminal_object_terminal := _ |}.
+
+(** The zero morphism between any two objects is the unique morphism
+    that factors through the zero object. *)
+
+Definition zero_morphism {C : PreCategory} {Z : ZeroObject C} (X Y : object C)
+  : morphism C X Y
+  := morphism_from_initial Y o morphism_to_terminal X.
+
+Arguments zero_morphism {C Z} X Y : simpl never.
+
+(** * Basic properties of zero objects *)
+
+(** ** Properties of zero morphisms *)
+
+(** Any morphism that factors through a zero object is the zero morphism. *)
+Lemma morphism_through_zero_is_zero {C : PreCategory} 
+  {Z : ZeroObject C} {X Y : object C}
+  (f : morphism C X Z)
+  (g : morphism C Z Y)
+  : (g o f)%morphism = zero_morphism X Y.
+Proof.
+  unfold zero_morphism.
+  apply ap011.
+  - rapply initial_morphism_unique.
+  - rapply terminal_morphism_unique.
+Qed.
+
+(** ** Composition properties of zero morphisms *)
+
+(** Composition with zero morphism on the right. *)
+Lemma zero_morphism_right {C : PreCategory} {Z : ZeroObject C}
+  {X Y W : object C}
+  (g : morphism C Y W)
+  : (g o zero_morphism X Y)%morphism = zero_morphism X W.
+Proof.
+  rewrite <- Category.Core.associativity.
+  apply morphism_through_zero_is_zero.
+Qed.
+
+(** Composition with zero morphism on the left. *)
+Lemma zero_morphism_left {C : PreCategory} {Z : ZeroObject C}
+  {X Y W : object C}
+  (f : morphism C X Y)
+  : (zero_morphism Y W o f)%morphism = zero_morphism X W.
+Proof.
+  rewrite Category.Core.associativity.
+  apply morphism_through_zero_is_zero.
+Qed.
+
+(** ** Export hints *)
+
+Hint Rewrite @zero_morphism_left @zero_morphism_right : zero_morphism.
diff --git a/theories/Categories/Category/Objects.v b/theories/Categories/Category/Objects.v
index cf4887b30a..7a148dde2b 100644
--- a/theories/Categories/Category/Objects.v
+++ b/theories/Categories/Category/Objects.v
@@ -23,13 +23,13 @@ Definition unique_up_to_unique_isomorphism (C : PreCategory) (P : C -> Type) :=
 Notation IsTerminalObject C x :=
   (forall x' : object C, Contr (morphism C x' x)).
 
-Record TerminalObject (C : PreCategory) :=
+Class TerminalObject (C : PreCategory) :=
   {
-    object_terminal :> C;
-    isterminal_object_terminal :> IsTerminalObject C object_terminal
+    object_terminal : C;
+    isterminal_object_terminal :: IsTerminalObject C object_terminal
   }.
 
-Existing Instance isterminal_object_terminal.
+Coercion object_terminal : TerminalObject >-> object.
 
 (** ** Initial objects *)
 (** An initial object is an object with a unique morphism from every
@@ -37,27 +37,27 @@ Existing Instance isterminal_object_terminal.
 Notation IsInitialObject C x :=
   (forall x' : object C, Contr (morphism C x x')).
 
-Record InitialObject (C : PreCategory) :=
+Class InitialObject (C : PreCategory) :=
   {
-    object_initial :> C;
-    isinitial_object_initial :> IsInitialObject C object_initial
+    object_initial : C;
+    isinitial_object_initial :: IsInitialObject C object_initial
   }.
 
-Existing Instance isinitial_object_initial.
+Coercion object_initial : InitialObject >-> object.
 
 Arguments unique_up_to_unique_isomorphism [C] P.
 
 (** ** Canonical morphisms *)
   
 (** The unique morphism from an initial object. *)
-Definition map_from_initial {C : PreCategory} {I : object C}
-  `{IsInitialObject C I} (Y : object C)
+Definition morphism_from_initial {C : PreCategory} {I : InitialObject C}
+  (Y : object C)
   : morphism C I Y
   := center (morphism C I Y).
-  
+
 (** The unique morphism to a terminal object. *)
-Definition map_to_terminal {C : PreCategory} {T : object C}
-  `{IsTerminalObject C T} (X : object C)
+Definition morphism_to_terminal {C : PreCategory} {T : TerminalObject C}
+  (X : object C)
   : morphism C X T
   := center (morphism C X T).