diff --git a/theories/base.v b/theories/base.v
index 9a066b9834084fa8353de3fa25b86d481a68bc11..83847b691a6b9450b9022e0178be499aeba9b791 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -591,6 +591,13 @@ Instance unit_leibniz : LeibnizEquiv unit.
 Proof. intros [] []; reflexivity. Qed.
 Instance unit_inhabited: Inhabited unit := populate ().
 
+(** ** Empty *)
+Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
+Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
+Proof. repeat split. Qed.
+Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
+Proof. intros [] []; reflexivity. Qed.
+
 (** ** Products *)
 Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.