From b93018cf39dab559072ba366aa0483b232ca7481 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Thu, 2 Nov 2023 13:32:08 +0100
Subject: [PATCH] Update Cubical/Foundations/Equiv.agda

---
 Cubical/Foundations/Equiv.agda | 1 -
 1 file changed, 1 deletion(-)

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