diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c2da2ff952eab94d4b891a4ff9553f02cf07e05d..599957ba0f1e2032694c216ffaf411e7e26376d8 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -9,7 +9,7 @@ Section sum.
   Context `{typeG Σ}.
 
   Program Definition emp : type :=
-    {| ty_size := 1%nat;
+    {| ty_size := 1%nat; (* This is 1 so that emp is equal to the empty sum. *)
        ty_own tid vl := False%I;
        ty_shr κ tid l := False%I |}.
   Next Obligation. iIntros (tid vl) "[]". Qed.