diff --git a/Categories/Adjoint.agda b/Categories/Adjoint.agda
index 4b3aa353c..3dc50ce30 100644
--- a/Categories/Adjoint.agda
+++ b/Categories/Adjoint.agda
@@ -3,7 +3,7 @@ module Categories.Adjoint where
 
 -- Adjoints
 
-open import Level using (Level; _⊔_)
+open import Level using (Level; _⊔_; levelOfTerm)
 
 open import Data.Product using (_,_; _×_)
 open import Function using () renaming (_∘_ to _∙_)
@@ -11,7 +11,7 @@ open import Function.Inverse using (Inverse)
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
 -- be explicit in imports to 'see' where the information comes from
-open import Categories.Category using (Category; levelOf)
+open import Categories.Category using (Category)
 open import Categories.Category.Product using (Product; _⁂_)
 open import Categories.Category.Instance.Setoids
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
@@ -27,7 +27,7 @@ private
     o ℓ e : Level
     C D : Category o ℓ e
 
-record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOf C ⊔ levelOf D) where
+record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm C ⊔ levelOfTerm D) where
   private
     module C = Category C
     module D = Category D
diff --git a/Categories/Category.agda b/Categories/Category.agda
index 60a0d9ed9..c59c45abd 100644
--- a/Categories/Category.agda
+++ b/Categories/Category.agda
@@ -20,7 +20,3 @@ _[_≈_] = Category._≈_
 
 _[_∘_] : ∀ {o ℓ e} → (C : Category o ℓ e) → ∀ {X Y Z} (f : C [ Y , Z ]) → (g : C [ X , Y ]) → C [ X , Z ]
 _[_∘_] = Category._∘_
-
--- Currently defined here for easier level polymorphism, but should move to main library
-levelOf : ∀ {o ℓ e} → Category o ℓ e → Level
-levelOf {o} {ℓ} {e} _ = o ⊔ ℓ ⊔ e
diff --git a/Categories/Category/Cartesian.agda b/Categories/Category/Cartesian.agda
index e68847414..e9ec23efd 100644
--- a/Categories/Category/Cartesian.agda
+++ b/Categories/Category/Cartesian.agda
@@ -30,7 +30,7 @@ private
     A B C D X Y Z : Obj
     f f′ g g′ h i : A ⇒ B
 
-record BinaryProducts : Set (levelOf 𝒞) where
+record BinaryProducts : Set (levelOfTerm 𝒞) where
 
   infixr 5 _×_
   infix 8 _⁂_
@@ -238,7 +238,7 @@ record BinaryProducts : Set (levelOf 𝒞) where
   _×- = appˡ -×-
 
 -- Cartesian monoidal category
-record Cartesian : Set (levelOf 𝒞) where
+record Cartesian : Set (levelOfTerm 𝒞) where
   field
     terminal : Terminal
     products : BinaryProducts
diff --git a/Categories/Category/CartesianClosed.agda b/Categories/Category/CartesianClosed.agda
index d76fa6bb0..f4087d588 100644
--- a/Categories/Category/CartesianClosed.agda
+++ b/Categories/Category/CartesianClosed.agda
@@ -28,7 +28,7 @@ private
 
 -- Cartesian closed category
 --   is a category with all products and exponentials
-record CartesianClosed : Set (levelOf 𝒞) where
+record CartesianClosed : Set (levelOfTerm 𝒞) where
   infixl 7 _^_
   
   field
diff --git a/Categories/Category/Monoidal/Braided.agda b/Categories/Category/Monoidal/Braided.agda
index e8145cab8..83d842bac 100644
--- a/Categories/Category/Monoidal/Braided.agda
+++ b/Categories/Category/Monoidal/Braided.agda
@@ -5,6 +5,8 @@ open import Categories.Category.Monoidal
 
 module Categories.Category.Monoidal.Braided {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where
 
+open import Level
+
 open import Data.Product using (Σ; _,_)
 
 open import Categories.Functor.Bifunctor
@@ -20,7 +22,7 @@ private
 -- braided monoidal category
 -- it has a braiding natural isomorphism has two hexagon identities.
 -- these two identities are directly expressed in the morphism level.
-record Braided : Set (levelOf C) where
+record Braided : Set (levelOfTerm C) where
   open Monoidal M public
 
   field
diff --git a/Categories/Category/Monoidal/Symmetric.agda b/Categories/Category/Monoidal/Symmetric.agda
index ac59046f7..e55cceda1 100644
--- a/Categories/Category/Monoidal/Symmetric.agda
+++ b/Categories/Category/Monoidal/Symmetric.agda
@@ -5,6 +5,8 @@ open import Categories.Category.Monoidal
 
 module Categories.Category.Monoidal.Symmetric {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where
 
+open import Level
+
 open import Data.Product using (Σ; _,_)
 
 open import Categories.Functor.Bifunctor
@@ -21,7 +23,7 @@ private
 
 -- symmetric monoidal category
 -- commutative braided monoidal category
-record Symmetric : Set (levelOf C) where
+record Symmetric : Set (levelOfTerm C) where
   field
     braided : Braided
 
diff --git a/Categories/Category/Monoidal/Traced.agda b/Categories/Category/Monoidal/Traced.agda
index 1f0d74314..56badb7a9 100644
--- a/Categories/Category/Monoidal/Traced.agda
+++ b/Categories/Category/Monoidal/Traced.agda
@@ -7,6 +7,8 @@ module Categories.Category.Monoidal.Traced {o ℓ e} {C : Category o ℓ e} (M :
 
 open Category C
 
+open import Level
+
 open import Data.Product using (_,_)
 
 open import Categories.Category.Monoidal.Symmetric M
@@ -37,7 +39,7 @@ private
 -- 
 -- note that the definition in this library is significantly easier than the previous one because
 -- we adopt a simpler definition of monoidal category to begin with.
-record Traced : Set (levelOf C) where
+record Traced : Set (levelOfTerm C) where
   field
     symmetric : Symmetric