Update Cubical/Foundations/Equiv.agda

agda · Nov 2, 2023 · cba9ebc · cba9ebc
1 parent b93018c
commit cba9ebc
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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
 
-          ((x : A) → PathP (B x) (f x) (g x)) ≃ PathP (λ i → (x : A) → B x i) f g
 funExt≃ {A = A}{B = B} {f = f} {g = g} = isoToEquiv e
   where
   open Iso