Restrict imports in Categories.Category.Construction.DaggerFunctors

agda · May 29, 2024 · 7cb0263 · 7cb0263
1 parent 9988022
commit 7cb0263
Showing 1 changed file with 6 additions and 7 deletions.
diff --git a/src/Categories/Category/Construction/DaggerFunctors.agda b/src/Categories/Category/Construction/DaggerFunctors.agda
@@ -2,18 +2,17 @@
 
 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
     o ℓ e o′ ℓ′ e′ : Level
 
 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
-