diff --git a/src/AG/Projective.ard b/src/AG/Projective.ard
index 2d04ad20..39c20713 100644
--- a/src/AG/Projective.ard
+++ b/src/AG/Projective.ard
@@ -24,7 +24,7 @@
 \import Data.Bool
 \import Data.Maybe
 \import Data.Or
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import HLevel
 \import Logic
diff --git a/src/AG/Scheme.ard b/src/AG/Scheme.ard
index 9e900b0d..978a5354 100644
--- a/src/AG/Scheme.ard
+++ b/src/AG/Scheme.ard
@@ -21,7 +21,7 @@
 \import Data.Array
 \import Data.Bool
 \import Data.Maybe
-\import Equiv \hiding (Map)
+\import Equiv
 \import Equiv.Fiber
 \import Equiv.Path
 \import Equiv.Sigma
diff --git a/src/Algebra/Module/FinModule.ard b/src/Algebra/Module/FinModule.ard
index a5331a00..2878dec9 100644
--- a/src/Algebra/Module/FinModule.ard
+++ b/src/Algebra/Module/FinModule.ard
@@ -8,7 +8,7 @@
 \import Arith.Nat
 \import Category
 \import Data.Array
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function \hiding (id, o)
 \import Function.Meta
 \import Logic
diff --git a/src/Algebra/Ring/Category.ard b/src/Algebra/Ring/Category.ard
index dc9b582f..1900da77 100644
--- a/src/Algebra/Ring/Category.ard
+++ b/src/Algebra/Ring/Category.ard
@@ -11,7 +11,7 @@
 \import Category.Limit
 \import Category.Meta
 \import Category.Subcat
-\import Equiv \hiding (Map)
+\import Equiv
 \import Logic
 \import Logic.FirstOrder.Algebraic
 \import Logic.FirstOrder.Algebraic.Category
diff --git a/src/Algebra/Ring/MPoly.ard b/src/Algebra/Ring/MPoly.ard
index bc8473b2..ebbe0f73 100644
--- a/src/Algebra/Ring/MPoly.ard
+++ b/src/Algebra/Ring/MPoly.ard
@@ -16,7 +16,7 @@
 \import Category
 \import Data.Array
 \import Data.Fin \hiding (Index)
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function (isSurj)
 \import Function.Meta ($)
 \import Logic
diff --git a/src/Category/Adjoint.ard b/src/Category/Adjoint.ard
index 8839f79e..2ec11c41 100644
--- a/src/Category/Adjoint.ard
+++ b/src/Category/Adjoint.ard
@@ -1,6 +1,6 @@
 \import Category
 \import Category.Functor
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Meta
 \import Paths
diff --git a/src/Category/Factorization.ard b/src/Category/Factorization.ard
index 9e55d04b..d01cefa4 100644
--- a/src/Category/Factorization.ard
+++ b/src/Category/Factorization.ard
@@ -1,6 +1,6 @@
 \import Category
 \import Category.Limit
-\import Equiv \hiding (Map)
+\import Equiv
 \import Logic
 \import Paths
 \import Paths.Meta
diff --git a/src/Category/Functor.ard b/src/Category/Functor.ard
index ff1fc83c..e88e9e0a 100644
--- a/src/Category/Functor.ard
+++ b/src/Category/Functor.ard
@@ -1,6 +1,6 @@
 \import Algebra.Meta
 \import Category
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Logic.Meta
 \import Meta
diff --git a/src/Category/Limit.ard b/src/Category/Limit.ard
index a475fb15..55b81707 100644
--- a/src/Category/Limit.ard
+++ b/src/Category/Limit.ard
@@ -3,7 +3,7 @@
 \import Category.Functor
 \import Category.Slice
 \import Data.Bool
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Logic
 \import Logic.Meta
diff --git a/src/Category/Subcat.ard b/src/Category/Subcat.ard
index ffb23e9b..e90d5234 100644
--- a/src/Category/Subcat.ard
+++ b/src/Category/Subcat.ard
@@ -2,7 +2,7 @@
 \import Category.Adjoint
 \import Category.Functor
 \import Category.Limit
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Homotopy.Fibration
 \import Meta
diff --git a/src/Category/Subobj.ard b/src/Category/Subobj.ard
index 01fa5f00..afefbb3e 100644
--- a/src/Category/Subobj.ard
+++ b/src/Category/Subobj.ard
@@ -1,6 +1,6 @@
 \import Category
 \import Category.Limit
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Logic
 \import Logic.Meta
diff --git a/src/Category/Topos/Sheaf.ard b/src/Category/Topos/Sheaf.ard
index 437eb2e2..fb2f76f8 100644
--- a/src/Category/Topos/Sheaf.ard
+++ b/src/Category/Topos/Sheaf.ard
@@ -5,7 +5,7 @@
 \import Category.Slice
 \import Category.Subcat
 \import Category.Topos.Sheaf.Site
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta
 \import Logic
 \import Logic.Meta
diff --git a/src/Set/Category.ard b/src/Set/Category.ard
index a7dcd56f..0128dc5d 100644
--- a/src/Set/Category.ard
+++ b/src/Set/Category.ard
@@ -3,7 +3,7 @@
 \import Category
 \import Category.Functor
 \import Category.Limit
-\import Equiv \hiding (Map)
+\import Equiv
 \import Function.Meta ($)
 \import HLevel
 \import Logic