Do not re-export FromStdLib

Saizan · Dec 2, 2017 · 62a3287 · 62a3287
1 parent ca840ce
commit 62a3287
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 5 deletions.
diff --git a/src/Cubical/GradLemma.agda b/src/Cubical/GradLemma.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical --postfix-projections #-}
 module Cubical.GradLemma where
 
-open import Cubical.PathPrelude
+open import Cubical
+open import Cubical.FromStdLib
 
 Square : ∀ {ℓ} {A : Set ℓ} {a0 a1 b0 b1 : A}
           (u : a0 ≡ a1) (v : b0 ≡ b1) (r0 : a0 ≡ b0) (r1 : a1 ≡ b1) → Set ℓ

diff --git a/src/Cubical/PathPrelude.agda b/src/Cubical/PathPrelude.agda
@@ -3,7 +3,7 @@ module Cubical.PathPrelude where
 
 open import Cubical.Primitives public
 open import Cubical.Primitives public using () renaming (Sub to _[_↦_])
-open import Cubical.FromStdLib public
+open import Cubical.FromStdLib
 
 module _ {ℓ} {A : Set ℓ} where
   refl : {x : A} → x ≡ x

diff --git a/src/Cubical/Retract.agda b/src/Cubical/Retract.agda
@@ -1,6 +1,7 @@
 module Cubical.Retract where
 
-open import Cubical.PathPrelude
+open import Cubical
+open import Cubical.FromStdLib
 
 section : ∀ {ℓa ℓb} → {A : Set ℓa} → {B : Set ℓb} → (f : A → B) → (g : B → A) → Set ℓb
 section f g = ∀ b → f (g b) ≡ b

diff --git a/src/Cubical/Sub.agda b/src/Cubical/Sub.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical #-}
 module Cubical.Sub where
 
-open import Cubical.PathPrelude
+open import Cubical
+open import Cubical.FromStdLib
 
 -- "Sub A φ t" is another notation for "A[φ ↦ t]" as a type.
 

diff --git a/src/Cubical/Univalence.agda b/src/Cubical/Univalence.agda
@@ -1,7 +1,8 @@
 {-# OPTIONS --cubical  #-}
 module Cubical.Univalence where
 
-open import Cubical.PathPrelude hiding (_≃_; idEquiv)
+open import Cubical hiding (_≃_; idEquiv)
+open import Cubical.FromStdLib
 open import Cubical.GradLemma
 open import Cubical.Retract