From f1cc0c4bd889e7bae702aa9dcbba9dfa001e93d8 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 6 Nov 2014 19:27:27 -0500
Subject: [PATCH] chore(library/hott) add note referring to missing
 substitution lemma

---
 library/hott/equiv.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 3522d6058..d1cd543fe 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