More selective import

fredefox · Mar 12, 2018 · 3a125a0 · 3a125a0
1 parent 84f16c1
commit 3a125a0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Cubical/PathPrelude.agda b/src/Cubical/PathPrelude.agda
@@ -7,7 +7,7 @@ open import Cubical.FromStdLib
 open import Cubical.NType public using (isContr ; isProp ; isSet)
 -- NB! This module does *not* use the same notion of equivalence `_≃_` as
 -- defined in Cubical.Equivalence!
-open import Cubical.Equivalence hiding (_≃_) public
+open import Cubical.Equivalence using (fiber ; isEquiv) public
 
 module _ {ℓ} {A : Set ℓ} where
   refl : {x : A} → x ≡ x