diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 3522d60588..d1cd543fea 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -285,9 +285,7 @@ namespace Equiv
   end
 
   -- calc enviroment
-  -- TODO: transport lemma without univalence?
-  -- theorem foo (P : Type → Type) (A B : Type) (H : A ≃ B) : P A → P B := sorry
-  -- calc_subst foo
+  -- Note: Calculating with substitutions needs univalence
   calc_trans compose
   calc_refl id
   calc_symm inv_closed