diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index b398aa9..42d63ab 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,7 +1,7 @@ {-# OPTIONS --cubical #-} module Cat.Categories.Rel where -open import Cubical.PathPrelude +open import Cubical open import Cubical.GradLemma open import Agda.Primitive open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 98750cf..181512c 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,6 +1,6 @@ module Cat.Categories.Sets where -open import Cubical.PathPrelude +open import Cubical open import Agda.Primitive open import Data.Product open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) diff --git a/src/Cat/Category/Bij.agda b/src/Cat/Category/Bij.agda index 0892f55..c611c6c 100644 --- a/src/Cat/Category/Bij.agda +++ b/src/Cat/Category/Bij.agda @@ -2,7 +2,7 @@ module Cat.Category.Bij where -open import Cubical.PathPrelude hiding ( Id ) +open import Cubical hiding ( Id ) open import Cubical.FromStdLib module _ {A : Set} {a : A} {P : A → Set} where diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index ff06743..5686356 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -1,7 +1,7 @@ module Cat.Category.Free where open import Agda.Primitive -open import Cubical.PathPrelude hiding (Path) +open import Cubical hiding (Path) open import Data.Product open import Cat.Category as C diff --git a/src/Cat/Category/Pathy.agda b/src/Cat/Category/Pathy.agda index e33a2ca..2764999 100644 --- a/src/Cat/Category/Pathy.agda +++ b/src/Cat/Category/Pathy.agda @@ -3,7 +3,7 @@ module Cat.Category.Pathy where open import Level -open import Cubical.PathPrelude +open import Cubical {- module _ {ℓ ℓ'} {A : Set ℓ} {x : A} diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 7056504..ff7d0ec 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -4,7 +4,7 @@ module Cat.Category.Properties where open import Agda.Primitive open import Data.Product -open import Cubical.PathPrelude +open import Cubical open import Cat.Category open import Cat.Functor