diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda
index 876c89029b..5d9fbe3726 100644
--- a/Cubical/Foundations/Equiv.agda
+++ b/Cubical/Foundations/Equiv.agda
@@ -319,7 +319,6 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f)
 
 -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv
 
-  where
   open Iso
   e : Iso ((x : A) → PathP (B x) (f x) (g x)) (PathP (λ i → (x : A) → B x i) f g)
   fun e p = funExt p