diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda index 798dd6deb0..5cf6fba008 100644 --- a/Cubical/Foundations/Everything.agda +++ b/Cubical/Foundations/Everything.agda @@ -28,7 +28,6 @@ open import Cubical.Foundations.Id ; isPropIsEquiv to isPropIsEquivId ) -open import Cubical.Foundations.GroupoidLaws public open import Cubical.Foundations.Function public open import Cubical.Foundations.Equiv public open import Cubical.Foundations.Equiv.Properties public