diff --git a/src/Categories/Category/Construction/DaggerFunctors.agda b/src/Categories/Category/Construction/DaggerFunctors.agda
index e16ac660..b9567fbb 100644
--- a/src/Categories/Category/Construction/DaggerFunctors.agda
+++ b/src/Categories/Category/Construction/DaggerFunctors.agda
@@ -2,13 +2,13 @@
 
 module Categories.Category.Construction.DaggerFunctors where
 
-open import Categories.Category.Core
-open import Categories.Category.Construction.Functors
-open import Categories.Category.SubCategory
-open import Categories.Category.Dagger
-open import Categories.Functor.Dagger
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Category.SubCategory using (FullSubCategory)
+open import Categories.Category.Dagger using (DaggerCategory)
+open import Categories.Functor.Dagger using (DaggerFunctor)
 
-open import Level
+open import Level using (Level; _⊔_)
 
 private
   variable
@@ -16,4 +16,3 @@ private
 
 DaggerFunctors : DaggerCategory o ℓ e → DaggerCategory o′ ℓ′ e′ → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
 DaggerFunctors C D = FullSubCategory (Functors (DaggerCategory.C C) (DaggerCategory.C D)) {I = DaggerFunctor C D} DaggerFunctor.functor
-