diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda
index c3a6e346db..0529733212 100644
--- a/Cubical/Foundations/Equiv.agda
+++ b/Cubical/Foundations/Equiv.agda
@@ -316,3 +316,6 @@ isEquiv-isEquiv'-Iso f .leftInv p i .equiv-proof = p .equiv-proof
 
 isEquiv≃isEquiv' : (f : A → B) → isEquiv f ≃ isEquiv' f
 isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f)
+
+-- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv
+