Update Cubical/Foundations/Equiv.agda

agda · Nov 2, 2023 · a07d092 · a07d092
1 parent f94ab37
commit a07d092
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Cubical/Foundations/Equiv.agda b/Cubical/Foundations/Equiv.agda
@@ -319,6 +319,5 @@ isEquiv≃isEquiv' f = isoToEquiv (isEquiv-isEquiv'-Iso f)
 
 -- The fact that funExt is an equivalence can be found in Cubical.Functions.FunExtEquiv
 
-  inv e p = funExt⁻ p
   rightInv e p = refl
   leftInv  e p = refl