diff --git a/theories/logrel/copying.v b/theories/logrel/copying.v
index 56e1968a04c8901ad8f7d2f9ce36b1f4abad1f9d..acc00305d90dcbe6443d29cfb82dc2684b07179c 100644
--- a/theories/logrel/copying.v
+++ b/theories/logrel/copying.v
@@ -23,6 +23,11 @@ Section copying.
     ⊢ copy A <: A.
   Proof. by iIntros (v) "!> #H". Qed.
 
+  (* TODO(COPY): have A <: copy- A rule *)
+  (* TODO(COPY): Show derived rules about copyability of products, sums, etc. *)
+  (* TODO(COPY): Commuting rule for μ, allowing `copy` to move outside the μ *)
+
+  (* TODO(COPY) *)
   Lemma coreP_desired_lemma (P : iProp Σ) :
     □ (P -∗ □ P) -∗ coreP P -∗ P.
   Proof.
@@ -102,7 +107,7 @@ Section copying.
         iExists A; repeat iModIntro; iApply "Hv".
   Qed.
 
-  (* TODO: Do the forall type former, once we have the value restriction *)
+  (* TODO(COPY) TODO(VALUERES): Do the forall type former, once we have the value restriction *)
 
   (* Copyability of recursive types *)
   Lemma lty_rec_copy C `{!Contractive C} :
diff --git a/theories/logrel/types.v b/theories/logrel/types.v
index 7380b53cfad5f4edebeb71cfabac354d763b8b61..5925e5670d0f0571dc38b6afc78063d3ed9eb523 100644
--- a/theories/logrel/types.v
+++ b/theories/logrel/types.v
@@ -472,7 +472,7 @@ Section properties.
     by iModIntro.
   Qed.
 
-  (* FIXME: copy *)
+  (* TODO(COPY) *)
   (* Lemma ltyped_load_copy A {copyA : LTyCopy A} : *)
   (*   ⊢ ∅ ⊨ load : ref_mut A → A * ref_mut A. *)
   (* Proof. *)
@@ -526,7 +526,7 @@ Section properties.
     by iExists m.
   Qed.
 
-  (* FIXME: copy *)
+  (* TODO(COPY) *)
   (* Lemma ltyped_ref_shr_load (A : lty Σ) {copyA : LTyCopy A} : *)
   (*   ⊢ ∅ ⊨ load : ref_shr A → (A * ref_shr A). *)
   (* Proof. *)