diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda index 38fbe86f99..fef7f76e32 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 -funExt≃ : {B : A → I → Type ℓ'} {f : (x : A) → B x i0} {g : (x : A) → B x i1} → ((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