cleaning importations

Author: jmougeot

src/Relation/Binary/Domain/Bundles.agda

@@ -6,20 +6,8 @@
 
 module Relation.Binary.Domain.Bundles where
 
+open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Bundles using (Poset)
-open import Relation.Binary.Core using (Rel)
-open import Level using (Level; _⊔_; suc; Lift; lift; lower)
-open import Function using (_∘_; id)
-open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
-open import Relation.Binary.Reasoning.PartialOrder
-open import Relation.Binary.Structures
-open import Data.Bool using (Bool; true; false; if_then_else_)
-open import Relation.Binary.Morphism.Structures
-open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
-open import Data.Nat.Properties using (≤-trans)
-
 open import Relation.Binary.Domain.Structures
 open import Relation.Binary.Domain.Definitions
 
@@ -45,7 +33,6 @@ module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
     open IsDCPO DcpoStr public
 
 module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ₁ ℓ₂} where
-
   private
     module P = Poset P
     module Q = Poset Q

src/Relation/Binary/Domain/Definitions.agda

@@ -6,17 +6,10 @@
 
 module Relation.Binary.Domain.Definitions where
 
+open import Data.Product using (∃-syntax; _×_; _,_)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Bundles using (Poset)
-open import Relation.Binary.Core using (Rel)
-open import Level using (Level; _⊔_; suc; Lift; lift; lower)
-open import Function using (_∘_; id)
-open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
-open import Relation.Binary.Reasoning.PartialOrder
-open import Relation.Binary.Morphism.Structures
 open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
-open import Data.Nat.Properties using (≤-trans)
 
 private variable
   c o ℓ e o' ℓ' e' ℓ₂ : Level
@@ -29,7 +22,6 @@ module _ where
 
 module _ {c ℓ₁ ℓ₂ : Level} (P : Poset c ℓ₁ ℓ₂) where
   open Poset P
-
   IsSemidirectedFamily : ∀ {Ix : Set c} → (s : Ix → Carrier) → Set _
   IsSemidirectedFamily s = ∀ i j → ∃[ k ] (s i ≤ s k × s j ≤ s k)
 

src/Relation/Binary/Domain/Structures.agda

@@ -6,19 +6,11 @@
 
 module Relation.Binary.Domain.Structures where
 
-open import Relation.Binary.Bundles using (Poset)
-open import Relation.Binary.Core using (Rel)
-open import Level using (Level; _⊔_; suc; Lift; lift; lower)
-open import Function using (_∘_; id)
-open import Data.Product using (∃-syntax; _×_; _,_; proj₁; proj₂)
-open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality using (_≡_; subst; cong)
-open import Relation.Binary.Reasoning.PartialOrder
-open import Relation.Binary.Structures
-open import Data.Bool using (Bool; true; false; if_then_else_)
-open import Relation.Binary.Morphism.Structures
-open import Relation.Binary.Morphism.Structures using (IsOrderHomomorphism)
+open import Data.Product using (_×_; _,_)
 open import Data.Nat.Properties using (≤-trans)
+open import Function using (_∘_)
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary.Bundles using (Poset)
 open import Relation.Binary.Domain.Definitions
 
 private variable