diff --git a/src/Category/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
similarity index 100%
rename from src/Category/Categories/Cat.agda
rename to src/Cat/Categories/Cat.agda
diff --git a/src/Category/Rel.agda b/src/Cat/Categories/Rel.agda
similarity index 94%
rename from src/Category/Rel.agda
rename to src/Cat/Categories/Rel.agda
index e9bbdc4..32e07f4 100644
--- a/src/Category/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -1,11 +1,14 @@
 {-# OPTIONS --cubical #-}
-module Category.Rel where
+module Cat.Categories.Rel where
 
-open import Data.Product
 open import Cubical.PathPrelude
 open import Cubical.GradLemma
 open import Agda.Primitive
-open import Category
+open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
+open import Function
+import Cubical.FromStdLib
+
+open import Cat.Category
 
 -- Subsets are predicates over some type.
 Subset : {ℓ : Level} → ( A : Set ℓ ) → Set (ℓ ⊔ lsuc lzero)
@@ -72,7 +75,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
         ≃ (a , b) ∈ S
-      equi = backwards , isequiv
+      equi = backwards Cubical.FromStdLib., isequiv
 
     ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S)
       ≡ (a , b) ∈ S
@@ -106,7 +109,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where
 
       equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
         ≃ ab ∈ S
-      equi = backwards , isequiv
+      equi = backwards Cubical.FromStdLib., isequiv
 
     ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B)
       ≡ ab ∈ S
@@ -144,7 +147,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset
 
     equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
       ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q))
-    equi = fwd , isequiv
+    equi = fwd Cubical.FromStdLib., isequiv
 
     -- assocc : Q + (R + S) ≡ (Q + R) + S
   is-assoc : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q)
diff --git a/src/Category/Sets.agda b/src/Cat/Categories/Sets.agda
similarity index 100%
rename from src/Category/Sets.agda
rename to src/Cat/Categories/Sets.agda
diff --git a/src/Category.agda b/src/Cat/Category.agda
similarity index 99%
rename from src/Category.agda
rename to src/Cat/Category.agda
index 568f93b..c3ce34f 100644
--- a/src/Category.agda
+++ b/src/Cat/Category.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --cubical #-}
 
-module Category where
+module Cat.Category where
 
 open import Agda.Primitive
 open import Data.Unit.Base
diff --git a/src/Category/Bij.agda b/src/Cat/Category/Bij.agda
similarity index 100%
rename from src/Category/Bij.agda
rename to src/Cat/Category/Bij.agda
diff --git a/src/Category/Free.agda b/src/Cat/Category/Free.agda
similarity index 100%
rename from src/Category/Free.agda
rename to src/Cat/Category/Free.agda
diff --git a/src/Category/Pathy.agda b/src/Cat/Category/Pathy.agda
similarity index 100%
rename from src/Category/Pathy.agda
rename to src/Cat/Category/Pathy.agda
diff --git a/src/Category/Cubical.agda b/src/Cat/Cubical.agda
similarity index 95%
rename from src/Category/Cubical.agda
rename to src/Cat/Cubical.agda
index 22709be..cba1c41 100644
--- a/src/Category/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -1,13 +1,14 @@
-module Category.Cubical where
+module Cat.Cubical where
 
 open import Agda.Primitive
-open import Category
 open import Data.Bool
 open import Data.Product
 open import Data.Sum
 open import Data.Unit
 open import Data.Empty
 
+open import Cat.Category
+
 module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
   -- Σ is the "namespace"
   ℓo = (lsuc lzero ⊔ ℓ)